Fermat's Last Theorem in Lean 4

Namespace `IsIntegral` 5 theorems

Eigenvalues on a finitely generated ℤ-lattice are integral IsIntegral.of_mem_span_of_apply_eq_smul 0 below · cited by 1 · depth 11
Adjoining an algebraic constant does not enlarge the span IsIntegral.mem_span_of_adjoin_simple_constants 0 below · cited by 1 · depth 16
Descent of integrality along a transcendental constant IsIntegral.mem_span_of_adjoin_simple_constants_transcendental 0 below · cited by 1 · depth 16
Denominator outside q for elements integral over B IsIntegral.exists_notMem_and_algebraMap_eq_mul_of_isIntegrallyClosed_localization_atPrime 0 below · cited by 1 · depth 27
Integrality detected modulo every prime ideal IsIntegral.of_forall_isPrime_isIntegral_quotient_mk 0 below · cited by 1 · depth 32

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.