Fermat's Last Theorem in Lean 4

Namespace `V3AsmLevel` 11 theorems

Special-fibre points with stalk dimension ≤ 1 are the η(v) V3AsmLevel.codim 55 below · cited by 1 · depth 18
Components of the resolved model have invertible ideal sheaves V3AsmLevel.comp_isInvertible 248 below · cited by 1 · depth 18
Product of component ideal sheaves on Y equals (q) V3AsmLevel.comp_prod 208 below · cited by 1 · depth 18
Distinct components meet only at chain edge points V3AsmLevel.edgePt_exhaust 186 below · cited by 1 · depth 18
Edge points lie on two consecutive chain components V3AsmLevel.edgePt_mem 1 below · cited by 1 · depth 18
Transversality of adjacent components at edge points V3AsmLevel.edgePt_transversal 188 below · cited by 1 · depth 18
Component ideals at the points η(v) of the glued model V3AsmLevel.eta_stalk 248 below · cited by 1 · depth 18
Rationality of the geometric exceptional fibres V3AsmLevel.exc_rational 8 below · cited by 1 · depth 18
Open smooth locus of the resolved model off the edge points V3AsmLevel.exists_smoothOffEdges 29 below · cited by 1 · depth 18
Components of the glued resolution are pulled back chart labels V3AsmLevel.label 201 below · cited by 1 · depth 18
Strict transforms have Igusa curves as geometric fibres V3AsmLevel.strict_iso 310 below · cited by 1 · depth 18

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.