Fermat's Last Theorem in Lean 4

Namespace `RingTheory` 5 theorems

Weak M-regularity transfers to sequences spanning a containing ideal RingTheory.Sequence.isWeaklyRegular_ofFn_of_isWeaklyRegular_ofFn_of_forall_mem_span 0 below · cited by 2 · depth 11
Regular pair on a finite algebra over a local ring RingTheory.Sequence.isRegular_pair_of_isSMulRegular_of_isReduced_of_forall_notMem_minimalPrimes 0 below · cited by 4 · depth 14
Vanishing of Tor₁(R/(x₁,…,xₙ),M) for weakly regular sequences RingTheory.Sequence.IsWeaklyRegular.isZero_tor_one_quotient_ofList 0 below · cited by 3 · depth 16
Weakly regular sequences on a nonzero free module RingTheory.Sequence.isWeaklyRegular_of_free 2 below · cited by 1 · depth 30
Weak regularity on a nonzero free module equals weak regularity on R RingTheory.Sequence.isWeaklyRegular_of_free_aux 1 below · cited by 1 · depth 31

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.