# Transfer algebraic structures across Equivs #

In this file we prove theorems of the following form: if β has a group structure and α ≃ β then α has a group structure, and similarly for monoids, semigroups, rings, integral domains, fields and so on.

Note that most of these constructions can also be obtained using the transport tactic.

### Implementation details #

When adding new definitions that transfer type-classes across an equivalence, please use abbrev. See note [reducible non-instances].

## Tags #

equiv, group, ring, field, module, algebra

@[reducible]
def Equiv.zero {α : Type u} {β : Type v} (e : α β) [Zero β] :
Zero α

Transfer Zero across an Equiv

Equations
• e.zero = { zero := e.symm 0 }
Instances For
@[reducible]
def Equiv.one {α : Type u} {β : Type v} (e : α β) [One β] :
One α

Transfer One across an Equiv

Equations
• e.one = { one := e.symm 1 }
Instances For
theorem Equiv.zero_def {α : Type u} {β : Type v} (e : α β) [Zero β] :
0 = e.symm 0
theorem Equiv.one_def {α : Type u} {β : Type v} (e : α β) [One β] :
1 = e.symm 1
noncomputable instance Equiv.instZeroShrink {α : Type u} [] [Zero α] :
Zero ()
Equations
• Equiv.instZeroShrink = ().symm.zero
noncomputable instance Equiv.instOneShrink {α : Type u} [] [One α] :
One ()
Equations
• Equiv.instOneShrink = ().symm.one
@[reducible]
def Equiv.add {α : Type u} {β : Type v} (e : α β) [Add β] :

Transfer Add across an Equiv

Equations
• e.add = { add := fun (x y : α) => e.symm (e x + e y) }
Instances For
@[reducible]
def Equiv.mul {α : Type u} {β : Type v} (e : α β) [Mul β] :
Mul α

Transfer Mul across an Equiv

Equations
• e.mul = { mul := fun (x y : α) => e.symm (e x * e y) }
Instances For
theorem Equiv.add_def {α : Type u} {β : Type v} (e : α β) [Add β] (x : α) (y : α) :
x + y = e.symm (e x + e y)
theorem Equiv.mul_def {α : Type u} {β : Type v} (e : α β) [Mul β] (x : α) (y : α) :
x * y = e.symm (e x * e y)
Equations
noncomputable instance Equiv.instMulShrink {α : Type u} [] [Mul α] :
Mul ()
Equations
• Equiv.instMulShrink = ().symm.mul
@[reducible]
def Equiv.sub {α : Type u} {β : Type v} (e : α β) [Sub β] :
Sub α

Transfer Sub across an Equiv

Equations
• e.sub = { sub := fun (x y : α) => e.symm (e x - e y) }
Instances For
@[reducible]
def Equiv.div {α : Type u} {β : Type v} (e : α β) [Div β] :
Div α

Transfer Div across an Equiv

Equations
• e.div = { div := fun (x y : α) => e.symm (e x / e y) }
Instances For
theorem Equiv.sub_def {α : Type u} {β : Type v} (e : α β) [Sub β] (x : α) (y : α) :
x - y = e.symm (e x - e y)
theorem Equiv.div_def {α : Type u} {β : Type v} (e : α β) [Div β] (x : α) (y : α) :
x / y = e.symm (e x / e y)
noncomputable instance Equiv.instSubShrink {α : Type u} [] [Sub α] :
Sub ()
Equations
• Equiv.instSubShrink = ().symm.sub
noncomputable instance Equiv.instDivShrink {α : Type u} [] [Div α] :
Div ()
Equations
• Equiv.instDivShrink = ().symm.div
@[reducible]
def Equiv.Neg {α : Type u} {β : Type v} (e : α β) [Neg β] :
Neg α

Transfer Neg across an Equiv

Equations
• e.Neg = { neg := fun (x : α) => e.symm (-e x) }
Instances For
@[reducible]
def Equiv.Inv {α : Type u} {β : Type v} (e : α β) [Inv β] :
Inv α

Transfer Inv across an Equiv

Equations
• e.Inv = { inv := fun (x : α) => e.symm (e x)⁻¹ }
Instances For
theorem Equiv.neg_def {α : Type u} {β : Type v} (e : α β) [Neg β] (x : α) :
-x = e.symm (-e x)
theorem Equiv.inv_def {α : Type u} {β : Type v} (e : α β) [Inv β] (x : α) :
x⁻¹ = e.symm (e x)⁻¹
noncomputable instance Equiv.instNegShrink {α : Type u} [] [Neg α] :
Neg ()
Equations
• Equiv.instNegShrink = ().symm.Neg
noncomputable instance Equiv.instInvShrink {α : Type u} [] [Inv α] :
Inv ()
Equations
• Equiv.instInvShrink = ().symm.Inv
@[reducible, inline]
abbrev Equiv.smul {α : Type u} {β : Type v} (e : α β) (R : Type u_1) [SMul R β] :
SMul R α

Transfer SMul across an Equiv

Equations
• e.smul R = { smul := fun (r : R) (x : α) => e.symm (r e x) }
Instances For
theorem Equiv.smul_def {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [SMul R β] (r : R) (x : α) :
r x = e.symm (r e x)
noncomputable instance Equiv.instSMulShrink {α : Type u} [] (R : Type u_1) [SMul R α] :
SMul R ()
Equations
• = ().symm.smul R
@[reducible]
def Equiv.pow {α : Type u} {β : Type v} (e : α β) (N : Type u_1) [Pow β N] :
Pow α N

Transfer Pow across an Equiv

Equations
• e.pow N = { pow := fun (x : α) (n : N) => e.symm (e x ^ n) }
Instances For
theorem Equiv.pow_def {α : Type u} {β : Type v} (e : α β) {N : Type u_1} [Pow β N] (n : N) (x : α) :
x ^ n = e.symm (e x ^ n)
noncomputable instance Equiv.instPowShrink {α : Type u} [] (N : Type u_1) [Pow α N] :
Pow () N
Equations
• = ().symm.pow N
theorem Equiv.addEquiv.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [Add β] (x : α) (y : α) :
e.toFun (x + y) = e.toFun x + e.toFun y
def Equiv.addEquiv {α : Type u} {β : Type v} (e : α β) [Add β] :
let mul := e.add; α ≃+ β

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.

Equations
Instances For
def Equiv.mulEquiv {α : Type u} {β : Type v} (e : α β) [Mul β] :
let mul := e.mul; α ≃* β

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.

Equations
• e.mulEquiv = let mul := e.mul; { toEquiv := e, map_mul' := }
Instances For
@[simp]
theorem Equiv.addEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] (a : α) :
@[simp]
theorem Equiv.mulEquiv_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (a : α) :
e.mulEquiv a = e a
theorem Equiv.addEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] (b : β) :
theorem Equiv.mulEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (b : β) :
(MulEquiv.symm e.mulEquiv) b = e.symm b
≃+ α

Shrink α to a smaller universe preserves addition.

Equations
Instances For
noncomputable def Shrink.mulEquiv {α : Type u} [] [Mul α] :
≃* α

Shrink α to a smaller universe preserves multiplication.

Equations
• Shrink.mulEquiv = ().symm.mulEquiv
Instances For
def Equiv.ringEquiv {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] :

An equivalence e : α ≃ β gives a ring equivalence α ≃+* β where the ring structure on α is the one obtained by transporting a ring structure on β back along e.

Equations
• e.ringEquiv = let add := e.add; let mul := e.mul; { toEquiv := e, map_mul' := , map_add' := }
Instances For
@[simp]
theorem Equiv.ringEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (a : α) :
e.ringEquiv a = e a
theorem Equiv.ringEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (b : β) :
(RingEquiv.symm e.ringEquiv) b = e.symm b
noncomputable def Shrink.ringEquiv (α : Type u) [] [Ring α] :
≃+* α

Shrink α to a smaller universe preserves ring structure.

Equations
• = ().symm.ringEquiv
Instances For
theorem Equiv.addSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.addSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer add_semigroup across an Equiv

Equations
Instances For
@[reducible]
def Equiv.semigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer Semigroup across an Equiv

Equations
• e.semigroup = let mul := e.mul;
Instances For
noncomputable instance Equiv.instAddSemigroupShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instSemigroupShrink {α : Type u} [] [] :
Equations
• Equiv.instSemigroupShrink = ().symm.semigroup
@[reducible, inline]
abbrev Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α β) :

Transfer SemigroupWithZero across an Equiv

Equations
• e.semigroupWithZero = let mul := e.mul; let zero := e.zero;
Instances For
noncomputable instance Equiv.instAddSemigroupWithZeroShrink {α : Type u} [] :
Equations
noncomputable instance Equiv.instSemigroupWithZeroShrink {α : Type u} [] :
Equations
• Equiv.instSemigroupWithZeroShrink = ().symm.semigroupWithZero
@[reducible]
def Equiv.addCommSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommSemigroup across an Equiv

Equations
Instances For
theorem Equiv.addCommSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.commSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommSemigroup across an Equiv

Equations
• e.commSemigroup = let mul := e.mul;
Instances For
noncomputable instance Equiv.instAddCommSemigroupShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instCommSemigroupShrink {α : Type u} [] [] :
Equations
• Equiv.instCommSemigroupShrink = ().symm.commSemigroup
@[reducible, inline]
abbrev Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulZeroClass across an Equiv

Equations
• e.mulZeroClass = let zero := e.zero; let mul := e.mul;
Instances For
noncomputable instance Equiv.instMulZeroClassShrink {α : Type u} [] [] :
Equations
• Equiv.instMulZeroClassShrink = ().symm.mulZeroClass
@[reducible]
def Equiv.addZeroClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddZeroClass across an Equiv

Equations
Instances For
theorem Equiv.addZeroClass.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
theorem Equiv.addZeroClass.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
@[reducible]
def Equiv.mulOneClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulOneClass across an Equiv

Equations
• e.mulOneClass = let one := e.one; let mul := e.mul;
Instances For
noncomputable instance Equiv.instAddZeroClassShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instMulOneClassShrink {α : Type u} [] [] :
Equations
• Equiv.instMulOneClassShrink = ().symm.mulOneClass
@[reducible, inline]
abbrev Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulZeroOneClass across an Equiv

Equations
• e.mulZeroOneClass = let zero := e.zero; let one := e.one; let mul := e.mul;
Instances For
noncomputable instance Equiv.instMulZeroOneClassShrink {α : Type u} [] [] :
Equations
• Equiv.instMulZeroOneClassShrink = ().symm.mulZeroOneClass
@[reducible]
def Equiv.addMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddMonoid across an Equiv

Equations
• e.addMonoid = let one := e.zero; let mul := e.add; let pow := e.smul ;
Instances For
theorem Equiv.addMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
theorem Equiv.addMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
@[reducible]
def Equiv.monoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer Monoid across an Equiv

Equations
• e.monoid = let one := e.one; let mul := e.mul; let pow := e.pow ;
Instances For
noncomputable instance Equiv.instAddMonoidShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instMonoidShrink {α : Type u} [] [] :
Equations
• Equiv.instMonoidShrink = ().symm.monoid
@[reducible]
def Equiv.addCommMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommMonoid across an Equiv

Equations
• e.addCommMonoid = let one := e.zero; let mul := e.add; let pow := e.smul ;
Instances For
theorem Equiv.addCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.commMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommMonoid across an Equiv

Equations
• e.commMonoid = let one := e.one; let mul := e.mul; let pow := e.pow ;
Instances For
noncomputable instance Equiv.instAddCommMonoidShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instCommMonoidShrink {α : Type u} [] [] :
Equations
• Equiv.instCommMonoidShrink = ().symm.commMonoid
theorem Equiv.addGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
@[reducible]
def Equiv.addGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddGroup across an Equiv

Equations
• e.addGroup = let one := e.zero; let mul := e.add; let inv := e.Neg; let div := e.sub; let npow := e.smul ; let zpow := e.smul ; Function.Injective.addGroup e
Instances For
theorem Equiv.addGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
theorem Equiv.addGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α), e (e.symm (-e x)) = -e x
theorem Equiv.addGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
@[reducible]
def Equiv.group {α : Type u} {β : Type v} (e : α β) [] :

Transfer Group across an Equiv

Equations
• e.group = let one := e.one; let mul := e.mul; let inv := e.Inv; let div := e.div; let npow := e.pow ; let zpow := e.pow ; Function.Injective.group e
Instances For
noncomputable instance Equiv.instAddGroupShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instGroupShrink {α : Type u} [] [] :
Equations
• Equiv.instGroupShrink = ().symm.group
theorem Equiv.addCommGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addCommGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
theorem Equiv.addCommGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
@[reducible]
def Equiv.addCommGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommGroup across an Equiv

Equations
• e.addCommGroup = let one := e.zero; let mul := e.add; let inv := e.Neg; let div := e.sub; let npow := e.smul ; let zpow := e.smul ; Function.Injective.addCommGroup e
Instances For
theorem Equiv.addCommGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α), e (e.symm (-e x)) = -e x
theorem Equiv.addCommGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
theorem Equiv.addCommGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
@[reducible]
def Equiv.commGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommGroup across an Equiv

Equations
• e.commGroup = let one := e.one; let mul := e.mul; let inv := e.Inv; let div := e.div; let npow := e.pow ; let zpow := e.pow ; Function.Injective.commGroup e
Instances For
noncomputable instance Equiv.instAddCommGroupShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instCommGroupShrink {α : Type u} [] [] :
Equations
• Equiv.instCommGroupShrink = ().symm.commGroup
@[reducible, inline]
abbrev Equiv.nonUnitalNonAssocSemiring {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalNonAssocSemiring across an Equiv

Equations
• e.nonUnitalNonAssocSemiring = let zero := e.zero; let add := e.add; let mul := e.mul; let nsmul := e.smul ;
Instances For
noncomputable instance Equiv.instNonUnitalNonAssocSemiringShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalNonAssocSemiringShrink = ().symm.nonUnitalNonAssocSemiring
@[reducible, inline]
abbrev Equiv.nonUnitalSemiring {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalSemiring across an Equiv

Equations
• e.nonUnitalSemiring = let zero := e.zero; let add := e.add; let mul := e.mul; let nsmul := e.smul ;
Instances For
noncomputable instance Equiv.instNonUnitalSemiringShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalSemiringShrink = ().symm.nonUnitalSemiring
@[reducible, inline]
abbrev Equiv.addMonoidWithOne {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddMonoidWithOne across an Equiv

Equations
Instances For
noncomputable instance Equiv.instAddMonoidWithOneShrink {α : Type u} [] [] :
Equations
@[reducible, inline]
abbrev Equiv.addGroupWithOne {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddGroupWithOne across an Equiv

Equations
Instances For
noncomputable instance Equiv.instAddGroupWithOneShrink {α : Type u} [] [] :
Equations
@[reducible, inline]
abbrev Equiv.nonAssocSemiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer NonAssocSemiring across an Equiv

Equations
Instances For
noncomputable instance Equiv.instNonAssocSemiringShrink {α : Type u} [] [] :
Equations
• Equiv.instNonAssocSemiringShrink = ().symm.nonAssocSemiring
@[reducible, inline]
abbrev Equiv.semiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer Semiring across an Equiv

Equations
• e.semiring = let mul := e.mul; let add_monoid_with_one := e.addMonoidWithOne; let npow := e.pow ; Function.Injective.semiring e
Instances For
noncomputable instance Equiv.instSemiringShrink {α : Type u} [] [] :
Equations
• Equiv.instSemiringShrink = ().symm.semiring
@[reducible, inline]
abbrev Equiv.nonUnitalCommSemiring {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalCommSemiring across an Equiv

Equations
• e.nonUnitalCommSemiring = let zero := e.zero; let add := e.add; let mul := e.mul; let nsmul := e.smul ;
Instances For
noncomputable instance Equiv.instNonUnitalCommSemiringShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalCommSemiringShrink = ().symm.nonUnitalCommSemiring
@[reducible, inline]
abbrev Equiv.commSemiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommSemiring across an Equiv

Equations
Instances For
noncomputable instance Equiv.instCommSemiringShrink {α : Type u} [] [] :
Equations
• Equiv.instCommSemiringShrink = ().symm.commSemiring
@[reducible, inline]
abbrev Equiv.nonUnitalNonAssocRing {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalNonAssocRing across an Equiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Equiv.instNonUnitalNonAssocRingShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalNonAssocRingShrink = ().symm.nonUnitalNonAssocRing
@[reducible, inline]
abbrev Equiv.nonUnitalRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer NonUnitalRing across an Equiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Equiv.instNonUnitalRingShrink {α : Type u} [] [] :
Equations
• Equiv.instNonUnitalRingShrink = ().symm.nonUnitalRing
@[reducible, inline]
abbrev Equiv.nonAssocRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer NonAssocRing across an Equiv

Equations
• e.nonAssocRing = let add_group_with_one := e.addGroupWithOne; let mul := e.mul; Function.Injective.nonAssocRing e
Instances For
noncomputable instance Equiv.instNonAssocRingShrink {α : Type u} [] [] :
Equations
• Equiv.instNonAssocRingShrink = ().symm.nonAssocRing
@[reducible, inline]
abbrev Equiv.ring {α : Type u} {β : Type v} (e : α β) [Ring β] :
Ring α

Transfer Ring across an Equiv

Equations
• e.ring = let mul := e.mul; let add_group_with_one := e.addGroupWithOne; let npow := e.pow ; Function.Injective.ring e
Instances For
noncomputable instance Equiv.instRingShrink {α : Type u} [] [Ring α] :
Ring ()
Equations
• Equiv.instRingShrink = ().symm.ring
@[reducible, inline]
abbrev Equiv.nonUnitalCommRing {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalCommRing across an Equiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Equiv.instNonUnitalCommRingShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalCommRingShrink = ().symm.nonUnitalCommRing
@[reducible, inline]
abbrev Equiv.commRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommRing across an Equiv

Equations
• e.commRing = let mul := e.mul; let add_group_with_one := e.addGroupWithOne; let npow := e.pow ; Function.Injective.commRing e
Instances For
noncomputable instance Equiv.instCommRingShrink {α : Type u} [] [] :
Equations
• Equiv.instCommRingShrink = ().symm.commRing
theorem Equiv.nontrivial {α : Type u} {β : Type v} (e : α β) [] :

Transfer Nontrivial across an Equiv

noncomputable instance Equiv.instNontrivialShrink {α : Type u} [] [] :
Equations
• =
theorem Equiv.isDomain {α : Type u} {β : Type v} [Ring α] [Ring β] [] (e : α ≃+* β) :

Transfer IsDomain across an Equiv

noncomputable instance Equiv.instIsDomainShrink {α : Type u} [] [Ring α] [] :
Equations
• =
@[reducible, inline]
abbrev Equiv.nnratCast {α : Type u} {β : Type v} (e : α β) [] :

Transfer NNRatCast across an Equiv

Equations
• e.nnratCast = { nnratCast := fun (q : ℚ≥0) => e.symm q }
Instances For
@[reducible, inline]
abbrev Equiv.ratCast {α : Type u} {β : Type v} (e : α β) [] :

Transfer RatCast across an Equiv

Equations
• e.ratCast = { ratCast := fun (n : ) => e.symm n }
Instances For
noncomputable instance Shrink.instNNRatCast {α : Type u} [] [] :
Equations
• Shrink.instNNRatCast = ().symm.nnratCast
noncomputable instance Shrink.instRatCast {α : Type u} [] [] :
Equations
• Shrink.instRatCast = ().symm.ratCast
@[reducible, inline]
abbrev Equiv.divisionRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer DivisionRing across an Equiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Equiv.instDivisionRingShrink {α : Type u} [] [] :
Equations
• Equiv.instDivisionRingShrink = ().symm.divisionRing
@[reducible, inline]
abbrev Equiv.field {α : Type u} {β : Type v} (e : α β) [] :

Transfer Field across an Equiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Equiv.instFieldShrink {α : Type u} [] [] :
Equations
• Equiv.instFieldShrink = ().symm.field
@[reducible, inline]
abbrev Equiv.mulAction {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] :

Transfer MulAction across an Equiv

Equations
• = let __src := e.smul R;
Instances For
noncomputable instance Equiv.instMulActionShrink {α : Type u} (R : Type u_1) [] [] [] :
Equations
@[reducible, inline]
abbrev Equiv.distribMulAction {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [] :

Transfer DistribMulAction across an Equiv

Equations
• = let __src := ;
Instances For
noncomputable instance Equiv.instDistribMulActionShrink {α : Type u} (R : Type u_1) [] [] [] [] :
Equations
@[reducible, inline]
abbrev Equiv.module {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] :
let addCommMonoid := e.addCommMonoid; [inst : Module R β] → Module R α

Transfer Module across an Equiv

Equations
• @Equiv.module α β R inst✝ e inst = let addCommMonoid := e.addCommMonoid; fun [Module R β] => let __src := ;
Instances For
noncomputable instance Equiv.instModuleShrink {α : Type u} (R : Type u_1) [] [] [] [Module R α] :
Module R ()
Equations
def Equiv.linearEquiv {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Module R β] :

An equivalence e : α ≃ β gives a linear equivalence α ≃ₗ[R] β where the R-module structure on α is the one obtained by transporting an R-module structure on β back along e.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Shrink.linearEquiv_symm_apply (α : Type u) (R : Type u_1) [] [] [] [Module R α] :
@[simp]
theorem Shrink.linearEquiv_apply (α : Type u) (R : Type u_1) [] [] [] [Module R α] :
∀ (a : ), () a = ().symm a
noncomputable def Shrink.linearEquiv (α : Type u) (R : Type u_1) [] [] [] [Module R α] :

Shrink α to a smaller universe preserves module structure.

Equations
Instances For
@[reducible, inline]
abbrev Equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] :
let semiring := e.semiring; [inst : Algebra R β] → Algebra R α

Transfer Algebra across an Equiv

Equations
Instances For
theorem Equiv.algebraMap_def {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Algebra R β] (r : R) :
let semiring := e.semiring; let algebra := ; () r = e.symm (() r)
noncomputable instance Equiv.instAlgebraShrink {α : Type u} (R : Type u_1) [] [] [] [Algebra R α] :
Algebra R ()
Equations
def Equiv.algEquiv {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Algebra R β] :
let semiring := e.semiring; let algebra := ; α ≃ₐ[R] β

An equivalence e : α ≃ β gives an algebra equivalence α ≃ₐ[R] β where the R-algebra structure on α is the one obtained by transporting an R-algebra structure on β back along e.

Equations
• = let semiring := e.semiring; let algebra := ; let __src := e.ringEquiv; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Equiv.algEquiv_apply {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Algebra R β] (a : α) :
() a = e a
theorem Equiv.algEquiv_symm_apply {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Algebra R β] (b : β) :
() b = e.symm b
@[simp]
theorem Shrink.algEquiv_apply (α : Type u) (R : Type u_1) [] [] [] [Algebra R α] :
∀ (a : ), () a = ().symm a
@[simp]
theorem Shrink.algEquiv_symm_apply (α : Type u) (R : Type u_1) [] [] [] [Algebra R α] :
∀ (a : α), ().symm a = () a
noncomputable def Shrink.algEquiv (α : Type u) (R : Type u_1) [] [] [] [Algebra R α] :

Shrink α to a smaller universe preserves algebra structure.

Equations
Instances For
theorem Finite.exists_type_zero_nonempty_mulEquiv (G : Type u) [] [] :
∃ (G' : Type) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

Any finite group in universe u is equivalent to some finite group in universe 0.