Normed groups conflict

Stream: maths

[Yaël Dillies]

Now that we have both additive and multiplicative normed groups and that they both use the same notation and naming convention, what do people think of adding something like the following?

class prenormed_space (α : Type*) extends pseudo_metric_space α, has_norm α :=
(exists_dist_eq_norm : ∃ a : α, ∀ b, dist a b = ∥b∥)

with of course a := 0 for additive normed groups and a := 1 for multiplicative ones.

[Yaël Dillies]

This gives us that the norm is nonnegative, and hopefully all other lemmas that are currently duplicated.

[Yaël Dillies]

This of course is mathematically uninteresting. It's just to avoid duplication in the parts of the API that transfers dist results to norm ones.

[Floris van Doorn]

Isn't @[to_additive] taking care of (most of) this duplication?

[Yaël Dillies]

Yes of course. But the lemma names are primed because the statement doesn't contain anything additive/multiplicative

[Floris van Doorn]

I see. And what kind of primed lemmas can you generalize to prenormed_space? Most lemmas I see refer to sub/zero (or div/one) explicitly

[Yaël Dillies]

docs#norm_nonneg, docs#bounded_iff_forall_norm_le, ...

[Yaël Dillies]

It won't be a lot, I must say.

[Jireh Loreaux]

In that case I would say let's not overburden type class inference by adding another intermediary.

[Eric Wieser]

It wouldn't need to be a true intermediary; typeclass inference ought only to be burdened by it for the lemmas Yaël has in mind. I'd hope for more than two though...