Fermat's Last Theorem in Lean 4

Namespace `MulSemiringAction` 2 theorems

Tate's splitting of a twisted semilinear pairing MulSemiringAction.exists_basis_extending_invariants_eq_zpow_smul_and_iff_mem_span_fixedPoints_of_pairing_of_continuous_cocycle 0 below · cited by 1 · depth 26
Element-wise orbit Chinese remainder for comaximal translates of P MulSemiringAction.mem_of_forall_smul_sub_mem_and_exists_forall_smul_sub_mem_of_forall_sup_smul_eq_top 0 below · cited by 9 · depth 29

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.