Mathlib v3 is deprecated. Go to Mathlib v4

Theorem map_eq_zero_iff_eq_one

Modification history

2023-01-09 19:56

src/algebra/order/hom/basic.lean

feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms (#16919) …

Modified map_eq_zero_iff_eq_one View on Github →

2022-09-12 13:12

src/analysis/normed/group/seminorm.lean

feat(analysis/normed/group/seminorm): Group norms (#16237) …

Added map_eq_zero_iff_eq_one View on Github →