mathlib
ef69cac1 - chore(topology/continuous_function/bounded): remove extra typeclass assumption (#10823)

Commit
4 years ago
chore(topology/continuous_function/bounded): remove extra typeclass assumption (#10823) Remove `[normed_star_monoid β]` from the typeclass assumptions of `[cstar_ring (α →ᵇ β)]` -- it was doing no harm, since it's implied by the assumption `[cstar_ring β]`, but it's unnecessary.
Author
Parents
Loading