Theorem Module.FaithfullyFlat.one_tmul_eq_zero_iff

Modification history

2025-03-17 19:45
Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
feat: generalize CommRing to Ring/Semiring (#22566) …
Modified Module.FaithfullyFlat.one_tmul_eq_zero_iffView on Github →
2025-01-17 19:10
Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)
Added Module.FaithfullyFlat.one_tmul_eq_zero_iffView on Github →