Fermat's Last Theorem in Lean 4

Namespace `V3Glue` 5 theorems

Étale charts over a reduced resolution give reduced pieces V3Glue.ChartInput.isReduced_Y 2 below · cited by 6 · depth 18
Glued components restrict to pullbacks of the model labels V3Glue.ChartInput.comap_iotaY_compG_chainPosPrime_eq 0 below · cited by 4 · depth 19
Points of the glued model with dim𝒪≤ 1 are η_G-points V3Glue.ChartInput.exists_eq_etaG_of_ringKrullDim_le_one 0 below · cited by 2 · depth 19
Base change of a glued component is isomorphic to R V3Glue.ChartInput.exists_iso_geometricFibre_strictTransform 1 below · cited by 1 · depth 19
Product of glued components restricts to (varpi) on the chart Yₙ V3Glue.ChartInput.prod_compG_comap_iotaY_eq 1 below · cited by 4 · depth 19

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.