Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-09 19:56 7ea60478

View on Github →

feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms (#16919) Generalise ..._seminorm_class to arbitrary codomains (rather than just ℝ). Instantiate mul_ring_norm_class for absolute values.

Estimated changes

added theorem abs_sub_map_le_div
added theorem le_map_add_map_div'
added theorem map_div_le_add
added theorem map_div_rev
added theorem map_eq_zero_iff_eq_one
added theorem map_ne_zero_iff_ne_one
added theorem map_pos_of_ne_one
deleted theorem abs_sub_map_le_div
deleted theorem le_map_add_map_div'
deleted theorem map_div_le_add
deleted theorem map_div_rev
deleted theorem map_eq_zero_iff_eq_one
deleted theorem map_ne_zero_iff_ne_one
deleted theorem map_pos_of_ne_one