Commit 2024-08-25 13:48 091f5d31

View on Github →

feat: The norm of a complex-valued AddChar (#15433) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

added theorem AddChar.coe_ne_zero

Modified Mathlib/Analysis/Normed/Field/Basic.lean

added theorem AddChar.norm_apply

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem AddChar.inv_apply_eq_conj

added theorem AddChar.map_neg_eq_conj