Commit 2021-06-22 19:52 c594196f
View on Github →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