Fermat's Last Theorem in Lean 4

Namespace `IsReduced` 5 theorems

Reducedness of A/(p) descends from B/pB IsReduced.quotient_span_singleton_of_injective_of_forall_exists_mul_mem 0 below · cited by 1 · depth 17
Base change to ℚ_ℓ preserves reducedness over ℤ IsReduced.padic_tensorProduct_of_moduleFinite_int 0 below · cited by 1 · depth 24
Reducedness of the image of a reduced finite-dimensional algebra IsReduced.range_of_finiteDimensional 0 below · cited by 1 · depth 24
Finite algebras with dim_K B points to K are reduced IsReduced.of_finrank_le_natCard_algHom 0 below · cited by 3 · depth 25
Reducedness of a closed fibre from its adic completions IsReduced.tensorProduct_residueField_of_forall_isMaximal_adicCompletion 0 below · cited by 2 · 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.