English
The equality (eq_1) states that for h and h', the corresponding NormedCommGroup.ofMulDist' equals the constructed structure with the proper fields and mul_comm.
Русский
Равенство eq_1 говорит, что для заданных h и h' соответствующая NormedCommGroup.ofMulDist' равна сконструированной структуре с нужными полями и mul_comm.
LaTeX
$$Eq (SeminormedCommGroup.ofMulDist' h₁ h₂) …$$
Lean4
/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
pseudometric space structure from the seminorm properties. Note that in most cases this instance
creates bad definitional equalities (e.g., it does not take into account a possibly existing
`UniformSpace` instance on `E`). -/
@[to_additive /-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing `UniformSpace` instance on `E`). -/
]
abbrev toSeminormedGroup [Group E] (f : GroupSeminorm E) : SeminormedGroup E
where
dist x y := f (x / y)
norm := f
dist_eq _ _ := rfl
dist_self x := by simp only [div_self', map_one_eq_zero]
dist_triangle := le_map_div_add_map_div f
dist_comm := map_div_rev f
