Theorem CharP.quotient'

Modification history

2023-08-10 19:52

Mathlib/Algebra/CharP/Quotient.lean

chore: banish `Type _` and `Sort _` (#6499) …

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 →