Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-14 06:59 23c61a3c

View on Github →

feat(analysis/normed/group/seminorm): add nonarchimedean (semi)norms (#17851) We introduce nonarchimedean seminorms and norms on additive groups.

Estimated changes

modified theorem add_group_seminorm.coe_smul
modified theorem group_norm.coe_le_coe
modified theorem group_norm.coe_lt_coe
modified theorem group_norm.coe_sup
modified theorem group_seminorm.coe_le_coe
modified theorem group_seminorm.coe_lt_coe
modified theorem group_seminorm.coe_sup
modified theorem group_seminorm.coe_zero
added theorem map_sub_le_max
added structure nonarch_add_group_norm