Commit 2025-11-02 21:27 e9311893

View on Github →

feat: characteristic of the quotient ring lies in the ideal (#31195) From CFT

Estimated changes

Modified Mathlib/Algebra/CharP/Quotient.lean

modified theorem CharP.ker_intAlgebraMap_eq_span

modified theorem CharP.quotient'

modified theorem CharP.quotient

modified theorem CharP.quotient_iff

modified theorem CharP.quotient_iff_le_ker_natCast

modified theorem Ideal.Quotient.index_eq_zero

added theorem Ideal.natCast_mem_of_charP_quotient