Theorem AddChar.coe_ne_zero

Modification history

2024-08-25 13:48
Mathlib/Algebra/Group/AddChar.lean
feat: The norm of a complex-valued `AddChar` (#15433) …
Added AddChar.coe_ne_zeroView on Github →