Skip to content

[Merged by Bors] - feat(RingTheory): let B be a faithfully flat A-algebra, then A is a local ring if B is#39611

Closed
mbkybky wants to merge 1 commit into
leanprover-community:masterfrom
mbkybky:Module.FaithfullyFlat.isLocalRing
Closed

[Merged by Bors] - feat(RingTheory): let B be a faithfully flat A-algebra, then A is a local ring if B is#39611
mbkybky wants to merge 1 commit into
leanprover-community:masterfrom
mbkybky:Module.FaithfullyFlat.isLocalRing

Update Algebra.lean

4da36c1
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
label-and-report-new-contributor
succeeded May 20, 2026 in 7s