Def add_monoid_hom.mk_normed_add_group_hom'

Modification history

2022-11-17 13:13
src/analysis/normed/group/hom.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified add_monoid_hom.mk_normed_add_group_hom'View on Github →
2022-07-24 16:34
src/analysis/normed/group/hom.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Added add_monoid_hom.mk_normed_add_group_hom'View on Github →