[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:masterleanprover-community/mathlib4:masterfrom

mbkybky:Module.FaithfullyFlat.isLocalRingmbkybky/mathlib4_my_fork:Module.FaithfullyFlat.isLocalRingCopy head branch name to clipboard