mathlib3

db107767 - chore(analysis/normed/field/unit_ball): cleanup instances (#15615)

chore(analysis/normed/field/unit_ball): cleanup instances (#15615) Add `subsemigroup.has_continuous_mul` and use it. Also use missing `ancestor` attributes so that `to_additive` works with `submonoid.to_subsemigroup`.