# 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, inline]
abbrev Equiv.zero {α : Type u} {β : Type v} (e : α β) [Zero β] :
Zero α

Transfer Zero across an Equiv

Equations
• e.zero = { zero := e.symm 0 }
Instances For
@[reducible, inline]
abbrev 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 α] :
Equations
noncomputable instance Equiv.instOneShrink {α : Type u} [] [One α] :
Equations
@[reducible, inline]
abbrev 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, inline]
abbrev 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 α] :
Equations
@[reducible, inline]
abbrev 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, inline]
abbrev 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 α] :
Equations
noncomputable instance Equiv.instDivShrink {α : Type u} [] [Div α] :
Equations
@[reducible, inline]
abbrev 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, inline]
abbrev 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 α] :
Equations
noncomputable instance Equiv.instInvShrink {α : Type u} [] [Inv α] :
Equations
@[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
@[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
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 = { 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
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 = { 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
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, inline]
abbrev Equiv.addSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer add_semigroup across an Equiv

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

Transfer Semigroup across an Equiv

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

Transfer SemigroupWithZero across an Equiv

Equations
• e.semigroupWithZero =
Instances For
noncomputable instance Equiv.instAddSemigroupWithZeroShrink {α : Type u} [] :
Equations
noncomputable instance Equiv.instSemigroupWithZeroShrink {α : Type u} [] :
Equations
• Equiv.instSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero
@[reducible, inline]
abbrev 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, inline]
abbrev Equiv.commSemigroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommSemigroup across an Equiv

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

Transfer MulZeroClass across an Equiv

Equations
• e.mulZeroClass =
Instances For
noncomputable instance Equiv.instMulZeroClassShrink {α : Type u} [] [] :
Equations
• Equiv.instMulZeroClassShrink = (equivShrink α).symm.mulZeroClass
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
@[reducible, inline]
abbrev Equiv.addZeroClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddZeroClass across an Equiv

Equations
Instances For
theorem Equiv.addZeroClass.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
@[reducible, inline]
abbrev Equiv.mulOneClass {α : Type u} {β : Type v} (e : α β) [] :

Transfer MulOneClass across an Equiv

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

Transfer MulZeroOneClass across an Equiv

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

Transfer AddMonoid across an Equiv

Equations
Instances For
theorem Equiv.addMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
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_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
@[reducible, inline]
abbrev Equiv.monoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer Monoid across an Equiv

Equations
• e.monoid =
Instances For
noncomputable instance Equiv.instAddMonoidShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instMonoidShrink {α : Type u} [] [] :
Equations
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_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
@[reducible, inline]
abbrev Equiv.addCommMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommMonoid across an Equiv

Equations
Instances For
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, inline]
abbrev Equiv.commMonoid {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommMonoid across an Equiv

Equations
• e.commMonoid =
Instances For
noncomputable instance Equiv.instAddCommMonoidShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instCommMonoidShrink {α : Type u} [] [] :
Equations
• Equiv.instCommMonoidShrink = (equivShrink α).symm.commMonoid
theorem Equiv.addGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [] :
e (e.symm 0) = 0
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_5 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
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_4 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
theorem Equiv.addGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α), e (e.symm (-e x)) = -e x
@[reducible, inline]
abbrev Equiv.addGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddGroup across an Equiv

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

Transfer Group across an Equiv

Equations
Instances For
noncomputable instance Equiv.instAddGroupShrink {α : Type u} [] [] :
Equations
noncomputable instance Equiv.instGroupShrink {α : Type u} [] [] :
Equations
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
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
theorem Equiv.addCommGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α), e (e.symm (-e x)) = -e x
@[reducible, inline]
abbrev Equiv.addCommGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer AddCommGroup across an Equiv

Equations
Instances For
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_6 {α : Type u_2} {β : Type u_1} (e : α β) [] :
∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
@[reducible, inline]
abbrev Equiv.commGroup {α : Type u} {β : Type v} (e : α β) [] :

Transfer CommGroup across an Equiv

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

Transfer NonUnitalNonAssocSemiring across an Equiv

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

Transfer NonUnitalSemiring across an Equiv

Equations
• e.nonUnitalSemiring =
Instances For
noncomputable instance Equiv.instNonUnitalSemiringShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalSemiringShrink = (equivShrink α).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 = (equivShrink α).symm.nonAssocSemiring
@[reducible, inline]
abbrev Equiv.semiring {α : Type u} {β : Type v} (e : α β) [] :

Transfer Semiring across an Equiv

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

Transfer NonUnitalCommSemiring across an Equiv

Equations
• e.nonUnitalCommSemiring =
Instances For
noncomputable instance Equiv.instNonUnitalCommSemiringShrink {α : Type u} [] :
Equations
• Equiv.instNonUnitalCommSemiringShrink = (equivShrink α).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 = (equivShrink α).symm.commSemiring
@[reducible, inline]
abbrev Equiv.nonUnitalNonAssocRing {α : Type u} {β : Type v} (e : α β) :

Transfer NonUnitalNonAssocRing across an Equiv

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

Transfer NonUnitalRing across an Equiv

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

Transfer NonAssocRing across an Equiv

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

Transfer Ring across an Equiv

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

Transfer NonUnitalCommRing across an Equiv

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

Transfer CommRing across an Equiv

Equations
Instances For
noncomputable instance Equiv.instCommRingShrink {α : Type u} [] [] :
Equations
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
noncomputable instance Shrink.instRatCast {α : Type u} [] [] :
Equations
@[reducible, inline]
abbrev Equiv.divisionRing {α : Type u} {β : Type v} (e : α β) [] :

Transfer DivisionRing across an Equiv

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

Transfer Field across an Equiv

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

Transfer MulAction across an Equiv

Equations
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
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
Instances For
noncomputable instance Equiv.instModuleShrink {α : Type u} (R : Type u_1) [] [] [] [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
• = { toFun := e.addEquiv.toFun, map_add' := , map_smul' := , invFun := e.addEquiv.invFun, left_inv := , right_inv := }
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 = (equivShrink α).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 := ; (algebraMap R α) r = e.symm ((algebraMap R β) r)
noncomputable instance Equiv.instAlgebraShrink {α : Type u} (R : Type u_1) [] [] [] [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
• = { toEquiv := e.ringEquiv.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 : α) :
(Equiv.algEquiv R e) a = e a
theorem Equiv.algEquiv_symm_apply {α : Type u} {β : Type v} (R : Type u_1) [] (e : α β) [] [Algebra R β] (b : β) :
(AlgEquiv.symm (Equiv.algEquiv R e)) b = e.symm b
@[simp]
theorem Shrink.algEquiv_apply (α : Type u) (R : Type u_1) [] [] [] [Algebra R α] :
∀ (a : ), (Shrink.algEquiv α R) a = (equivShrink α).symm a
@[simp]
theorem Shrink.algEquiv_symm_apply (α : Type u) (R : Type u_1) [] [] [] [Algebra R α] :
∀ (a : α), (Shrink.algEquiv α R).symm a = (equivShrink α) 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_univ_nonempty_mulEquiv (G : Type u) [] [] :
∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

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