mathlib
c594196f - chore(topology/continuous_function/algebra): delete old instances, use bundled sub[monoid, group, ring]s (#8004)

Commit
4 years ago
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
Author
Parents
Loading