Commit 2021-06-22 19:52 c594196f

chore(topology/continuous_function/algebra): delete old instances, use bundled sub[monoid, group, ring]s (#8004) We remove the monoid, group, ... instances on { f : α → β | continuous f } since C(α, β) should be used instead, and we replacce the sub[monoid, group, ...] instances on { f : α → β | continuous f } by definitions of bundled subobjects with carrier { f : α → β | continuous f }. We keep the set_of for subobjects since we need a subset to be the carrier. Zulip : https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/instances.20on.20continuous.20subtype