Transfer algebraic structures across Equiv
s #
In this file we prove lemmas of the following form: if β
has a group structure and α ≃ β
then α
has a group structure, and similarly for monoids, semigroups and so on.
Implementation details #
When adding new definitions that transfer type-classes across an equivalence, please use
abbrev
. See note [reducible non-instances].
An equivalence e : α ≃ β
gives a multiplicative equivalence α ≃* β
where
the multiplicative structure on α
is the one obtained by transporting a multiplicative structure
on β
back along e
.
Instances For
An equivalence e : α ≃ β
gives an additive equivalence α ≃+ β
where
the additive structure on α
is the one obtained by transporting an additive structure
on β
back along e
.
Instances For
Transfer add_semigroup
across an Equiv
Equations
- e.addSemigroup = Function.Injective.addSemigroup ⇑e ⋯ ⋯
Instances For
Transfer CommSemigroup
across an Equiv
Equations
Instances For
Transfer AddCommSemigroup
across an Equiv
Equations
Instances For
Transfer MulOneClass
across an Equiv
Equations
- e.mulOneClass = Function.Injective.mulOneClass ⇑e ⋯ ⋯ ⋯
Instances For
Transfer AddZeroClass
across an Equiv
Equations
- e.addZeroClass = Function.Injective.addZeroClass ⇑e ⋯ ⋯ ⋯
Instances For
Transfer CommMonoid
across an Equiv
Equations
- e.commMonoid = Function.Injective.commMonoid ⇑e ⋯ ⋯ ⋯ ⋯
Instances For
Transfer AddCommMonoid
across an Equiv
Equations
- e.addCommMonoid = Function.Injective.addCommMonoid ⇑e ⋯ ⋯ ⋯ ⋯
Instances For
Transfer AddCommGroup
across an Equiv
Equations
- e.addCommGroup = Function.Injective.addCommGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯