Theorem charZero_of_expChar_one'

Modification history

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 →