Fermat's Last Theorem in Lean 4

Namespace `ContinuousMap` 2 theorems

Characters inherit translation relations of a nonzero continuous function ContinuousMap.exists_continuous_monoidHom_forall_sum_eq_zero_of_compactSpace 3 below · cited by 2 · depth 17
Vanishing a.e. against a point-separating star subalgebra ContinuousMap.ae_eq_zero_of_forall_mem_starSubalgebra_integral_mul_eq_zero 0 below · cited by 3 · depth 22

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.