Fermat's Last Theorem in Lean 4

Namespace `IsFractionRing` 2 theorems

Fraction fields of a bijective base change IsFractionRing.bijective_tensorProduct_lift_of_bijective_baseChange 0 below · cited by 1 · depth 26
Inverse powers of a product of branch ideals: localisation and restriction IsFractionRing.exists_pow_mul_mem_colon_and_surjective_restrict_of_branchData 0 below · cited by 1 · depth 28

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.