Commit 2023-03-29 05:49 eb9d5a47

View on Github →

feat: port Algebra.CharP.Quotient (#3131)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharP/Quotient.lean

added theorem CharP.quotient'

added theorem CharP.quotient

added theorem Ideal.Quotient.index_eq_zero