Theorem charZero_of_expChar_one'

Modification history

2026-09-09 10:59
Mathlib/Algebra/CharP/Defs.lean
chore: missing CharP and CharZero instances for Matrix (#43550)
Modified charZero_of_expChar_one'View on Github →
2024-10-21 22:54
Mathlib/Algebra/CharP/Defs.lean
refactor: merge `ExpChar` and `CharP` API (#18023) …
Modified charZero_of_expChar_one'View on Github →
2023-11-01 16:07
Mathlib/Algebra/CharP/ExpChar.lean
chore: demote `charZero_of_expChar_one'` instance to a theorem (#7777) …
Added charZero_of_expChar_one'View on Github →