Theorem CharP.quotient

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 View on Github →

2023-03-29 05:49

Mathlib/Algebra/CharP/Quotient.lean

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

Added CharP.quotient View on Github →