Theorem CharP.quotient_iff_le_ker_natCast

Modification history

2025-11-02 21:27
Mathlib/Algebra/CharP/Quotient.lean
feat: characteristic of the quotient ring lies in the ideal (#31195) …
Modified CharP.quotient_iff_le_ker_natCastView on Github →
2023-10-23 14:19
Mathlib/Algebra/CharP/Quotient.lean
feat(Algebra/CharP/Quotient): iff lemmas (#7748)
Added CharP.quotient_iff_le_ker_natCastView on Github →