Fermat's Last Theorem in Lean 4

Namespace `CochainCx` 3 theorems

Injective Künneth map into total cohomology over a field CochainCx.Bounded.exists_kunneth_toModule_HTot_tensor_injective 0 below · cited by 2 · depth 34
Künneth dimension formula over a field for bounded cochain complexes CochainCx.Bounded.finrank_HTot_tensor_eq_sum_mul 5 below · cited by 1 · depth 34
Levelwise splitting of a bounded complex over a field CochainCx.Bounded.exists_contractible_levelwise_equiv_prod 0 below · cited by 1 · depth 35

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.