Fermat's Last Theorem in Lean 4

Namespace `CommRingCat` 2 theorems

Triple tensor product as a pushout of commutative rings CommRingCat.isPushout_tensorProduct_tensorProduct 0 below · cited by 1 · depth 34
Pushout squares over a fibre product of rings, surjective case CommRingCat.isPushout_of_isPullback_of_isPullback_of_isPushout_of_surjective 0 below · cited by 1 · depth 45

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.