Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.exists_isPrime_liesOver_of_faithfullyFlat
Modification history
2025-02-12 21:23
Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
feat(RingTheory/FaithfullyFlat): equivalent characterizations for algebras (#20725) …
Added
Ideal.exists_isPrime_liesOver_of_faithfullyFlat
View on Github →