Fermat's Last Theorem in Lean 4

Namespace `exteriorPower` 5 theorems

Top exterior power of multiplication by x is N_{B/A}(x) exteriorPower.map_mulLeft_apply_eq_norm_smul 2 below · cited by 1 · depth 15
Image of bigwedgeᵈ N in bigwedgeᵈ M for corank-one N over a DVR exteriorPower.range_map_subtype_eq_maximalIdeal_smul_top 0 below · cited by 1 · depth 15
Top exterior power of an endomorphism is multiplication by det exteriorPower.map_apply_eq_det_smul 1 below · cited by 1 · depth 16
Top wedge of images under an endomorphism is det f times the wedge exteriorPower.iotaMulti_comp_eq_det_smul 0 below · cited by 1 · depth 17
Exterior powers commute with base change exteriorPower.exists_linearEquiv_baseChange 0 below · cited by 1 · depth 34

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.