Theorem EqualCharZero.pnatCast_one

Modification history

2026-03-20 06:03
Mathlib/Algebra/CharP/MixedCharZero.lean
chore(Algebra/CharP/MixedCharZero): cleanup file and use module system (#34676) …
Deleted EqualCharZero.pnatCast_oneView on Github →
2023-05-21 13:23
Mathlib/Algebra/CharP/MixedCharZero.lean
feat: port Algebra.CharP.MixedCharZero (#3222)
Added EqualCharZero.pnatCast_oneView on Github →