Mathlib Changelog
v4
Changelog
About
Github
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