Commit 2022-09-15 21:54 97befb83

View on Github →

feat(analysis/normed/ring/seminorm): add ring_seminorm, ring_norm (#14115) We define structures ring_seminorm and ring_norm. These definitions are useful when one needs to consider multiple (semi)norms on a given ring.

Estimated changes

Modified docs/references.bib

Modified src/analysis/normed/group/basic.lean

added theorem coe_norm_add_group_norm

added def norm_add_group_norm

Modified src/analysis/normed/group/seminorm.lean

added theorem group_norm.to_fun_eq_coe

added theorem group_seminorm.to_fun_eq_coe

Created src/analysis/normed/ring/seminorm.lean

added def norm_ring_norm

added def norm_ring_seminorm

added theorem ring_norm.apply_one

added theorem ring_norm.ext

added theorem ring_norm.to_fun_eq_coe

added structure ring_norm

added theorem ring_seminorm.apply_one

added theorem ring_seminorm.eq_zero_iff

added theorem ring_seminorm.ext

added theorem ring_seminorm.ne_zero_iff

added theorem ring_seminorm.seminorm_one_eq_one_iff_ne_zero

added theorem ring_seminorm.to_fun_eq_coe

added def ring_seminorm.to_ring_norm

added structure ring_seminorm