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 mark them @[reducible]. 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

• Equiv.zero e = { zero := e.symm 0 }

@[reducible]

def Equiv.one {α : Type u} {β : Type v} (e : α ≃ β) [One β] : One α

Transfer One across an Equiv

Equations

• Equiv.one e = { one := e.symm 1 }

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} [Small.{v, u} α] [Zero α] : Zero (Shrink.{v, u} α)

Equations

• Equiv.instZeroShrink = Equiv.zero (equivShrink α).symm

noncomputable instance Equiv.instOneShrink {α : Type u} [Small.{v, u} α] [One α] : One (Shrink.{v, u} α)

Equations

• Equiv.instOneShrink = Equiv.one (equivShrink α).symm

@[reducible]

def Equiv.add {α : Type u} {β : Type v} (e : α ≃ β) [Add β] : Add α

Transfer Add across an Equiv

Equations

• Equiv.add e = { add := fun (x y : α) => e.symm (e x + e y) }

@[reducible]

def Equiv.mul {α : Type u} {β : Type v} (e : α ≃ β) [Mul β] : Mul α

Transfer Mul across an Equiv

Equations

• Equiv.mul e = { mul := fun (x y : α) => e.symm (e x * e y) }

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)

noncomputable instance Equiv.instAddShrink {α : Type u} [Small.{v, u} α] [Add α] : Add (Shrink.{v, u} α)

Equations

• Equiv.instAddShrink = Equiv.add (equivShrink α).symm

noncomputable instance Equiv.instMulShrink {α : Type u} [Small.{v, u} α] [Mul α] : Mul (Shrink.{v, u} α)

Equations

• Equiv.instMulShrink = Equiv.mul (equivShrink α).symm

@[reducible]

def Equiv.sub {α : Type u} {β : Type v} (e : α ≃ β) [Sub β] : Sub α

Transfer Sub across an Equiv

Equations

• Equiv.sub e = { sub := fun (x y : α) => e.symm (e x - e y) }

@[reducible]

def Equiv.div {α : Type u} {β : Type v} (e : α ≃ β) [Div β] : Div α

Transfer Div across an Equiv

Equations

• Equiv.div e = { div := fun (x y : α) => e.symm (e x / e y) }

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} [Small.{v, u} α] [Sub α] : Sub (Shrink.{v, u} α)

Equations

• Equiv.instSubShrink = Equiv.sub (equivShrink α).symm

noncomputable instance Equiv.instDivShrink {α : Type u} [Small.{v, u} α] [Div α] : Div (Shrink.{v, u} α)

Equations

• Equiv.instDivShrink = Equiv.div (equivShrink α).symm

@[reducible]

def Equiv.Neg {α : Type u} {β : Type v} (e : α ≃ β) [Neg β] : Neg α

Transfer Neg across an Equiv

Equations

• Equiv.Neg e = { neg := fun (x : α) => e.symm (-e x) }

@[reducible]

def Equiv.Inv {α : Type u} {β : Type v} (e : α ≃ β) [Inv β] : Inv α

Transfer Inv across an Equiv

Equations

• Equiv.Inv e = { inv := fun (x : α) => e.symm (e x)⁻¹ }

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} [Small.{v, u} α] [Neg α] : Neg (Shrink.{v, u} α)

Equations

• Equiv.instNegShrink = Equiv.Neg (equivShrink α).symm

noncomputable instance Equiv.instInvShrink {α : Type u} [Small.{v, u} α] [Inv α] : Inv (Shrink.{v, u} α)

Equations

• Equiv.instInvShrink = Equiv.Inv (equivShrink α).symm

@[reducible]

def Equiv.smul {α : Type u} {β : Type v} (e : α ≃ β) (R : Type u_1) [SMul R β] : SMul R α

Transfer SMul across an Equiv

Equations

• Equiv.smul e R = { smul := fun (r : R) (x : α) => e.symm (r • e x) }

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} [Small.{v, u} α] (R : Type u_1) [SMul R α] : SMul R (Shrink.{v, u} α)

Equations

• Equiv.instSMulShrink R = Equiv.smul (equivShrink α).symm R

@[reducible]

def Equiv.pow {α : Type u} {β : Type v} (e : α ≃ β) (N : Type u_1) [Pow β N] : Pow α N

Transfer Pow across an Equiv

Equations

• Equiv.pow e N = { pow := fun (x : α) (n : N) => e.symm (e x ^ n) }

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} [Small.{v, u} α] (N : Type u_1) [Pow α N] : Pow (Shrink.{v, u} α) N

Equations

• Equiv.instPowShrink N = Equiv.pow (equivShrink α).symm 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 := Equiv.add e; α ≃+ β

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

• Equiv.addEquiv e = let mul := Equiv.add e; { toEquiv := e, map_add' := ⋯ }

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

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

• Equiv.mulEquiv e = let mul := Equiv.mul e; { toEquiv := e, map_mul' := ⋯ }

@[simp]

theorem Equiv.addEquiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [Add β] (a : α) : (Equiv.addEquiv e) a = e a

@[simp]

theorem Equiv.mulEquiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [Mul β] (a : α) : (Equiv.mulEquiv e) a = e a

theorem Equiv.addEquiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [Add β] (b : β) : (AddEquiv.symm (Equiv.addEquiv e)) b = e.symm b

theorem Equiv.mulEquiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [Mul β] (b : β) : (MulEquiv.symm (Equiv.mulEquiv e)) b = e.symm b

noncomputable def Shrink.addEquiv {α : Type u} [Small.{v, u} α] [Add α] : Shrink.{v, u} α ≃+ α

Shrink α to a smaller universe preserves addition.

Equations

• Shrink.addEquiv = Equiv.addEquiv (equivShrink α).symm

noncomputable def Shrink.mulEquiv {α : Type u} [Small.{v, u} α] [Mul α] : Shrink.{v, u} α ≃* α

Shrink α to a smaller universe preserves multiplication.

Equations

• Shrink.mulEquiv = Equiv.mulEquiv (equivShrink α).symm

def Equiv.ringEquiv {α : Type u} {β : Type v} (e : α ≃ β) [Add β] [Mul β] : let add := Equiv.add e; let mul := Equiv.mul e; α ≃+* β

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

• Equiv.ringEquiv e = let add := Equiv.add e; let mul := Equiv.mul e; { toEquiv := e, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem Equiv.ringEquiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [Add β] [Mul β] (a : α) : (Equiv.ringEquiv e) a = e a

theorem Equiv.ringEquiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [Add β] [Mul β] (b : β) : (RingEquiv.symm (Equiv.ringEquiv e)) b = e.symm b

noncomputable def Shrink.ringEquiv (α : Type u) [Small.{v, u} α] [Ring α] : Shrink.{v, u} α ≃+* α

Shrink α to a smaller universe preserves ring structure.

Equations

• Shrink.ringEquiv α = Equiv.ringEquiv (equivShrink α).symm

theorem Equiv.addSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddSemigroup β] : ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y

@[reducible]

def Equiv.addSemigroup {α : Type u} {β : Type v} (e : α ≃ β) [AddSemigroup β] : AddSemigroup α

Transfer add_semigroup across an Equiv

Equations

• Equiv.addSemigroup e = let mul := Equiv.add e; Function.Injective.addSemigroup ⇑e ⋯ ⋯

@[reducible]

def Equiv.semigroup {α : Type u} {β : Type v} (e : α ≃ β) [Semigroup β] : Semigroup α

Transfer Semigroup across an Equiv

Equations

• Equiv.semigroup e = let mul := Equiv.mul e; Function.Injective.semigroup ⇑e ⋯ ⋯

noncomputable instance Equiv.instAddSemigroupShrink {α : Type u} [Small.{v, u} α] [AddSemigroup α] : AddSemigroup (Shrink.{v, u} α)

Equations

• Equiv.instAddSemigroupShrink = Equiv.addSemigroup (equivShrink α).symm

noncomputable instance Equiv.instSemigroupShrink {α : Type u} [Small.{v, u} α] [Semigroup α] : Semigroup (Shrink.{v, u} α)

Equations

• Equiv.instSemigroupShrink = Equiv.semigroup (equivShrink α).symm

@[reducible]

def Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α ≃ β) [SemigroupWithZero β] : SemigroupWithZero α

Transfer SemigroupWithZero across an Equiv

Equations

• Equiv.semigroupWithZero e = let mul := Equiv.mul e; let zero := Equiv.zero e; Function.Injective.semigroupWithZero ⇑e ⋯ ⋯ ⋯

noncomputable instance Equiv.instAddSemigroupWithZeroShrink {α : Type u} [Small.{v, u} α] [SemigroupWithZero α] : SemigroupWithZero (Shrink.{v, u} α)

Equations

• Equiv.instAddSemigroupWithZeroShrink = Equiv.semigroupWithZero (equivShrink α).symm

noncomputable instance Equiv.instSemigroupWithZeroShrink {α : Type u} [Small.{v, u} α] [SemigroupWithZero α] : SemigroupWithZero (Shrink.{v, u} α)

Equations

• Equiv.instSemigroupWithZeroShrink = Equiv.semigroupWithZero (equivShrink α).symm

@[reducible]

def Equiv.addCommSemigroup {α : Type u} {β : Type v} (e : α ≃ β) [AddCommSemigroup β] : AddCommSemigroup α

Transfer AddCommSemigroup across an Equiv

Equations

• Equiv.addCommSemigroup e = let mul := Equiv.add e; Function.Injective.addCommSemigroup ⇑e ⋯ ⋯

theorem Equiv.addCommSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommSemigroup β] : ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y

@[reducible]

def Equiv.commSemigroup {α : Type u} {β : Type v} (e : α ≃ β) [CommSemigroup β] : CommSemigroup α

Transfer CommSemigroup across an Equiv

Equations

• Equiv.commSemigroup e = let mul := Equiv.mul e; Function.Injective.commSemigroup ⇑e ⋯ ⋯

noncomputable instance Equiv.instAddCommSemigroupShrink {α : Type u} [Small.{v, u} α] [AddCommSemigroup α] : AddCommSemigroup (Shrink.{v, u} α)

Equations

• Equiv.instAddCommSemigroupShrink = Equiv.addCommSemigroup (equivShrink α).symm

noncomputable instance Equiv.instCommSemigroupShrink {α : Type u} [Small.{v, u} α] [CommSemigroup α] : CommSemigroup (Shrink.{v, u} α)

Equations

• Equiv.instCommSemigroupShrink = Equiv.commSemigroup (equivShrink α).symm

@[reducible]

def Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroClass β] : MulZeroClass α

Transfer MulZeroClass across an Equiv

Equations

• Equiv.mulZeroClass e = let zero := Equiv.zero e; let mul := Equiv.mul e; Function.Injective.mulZeroClass ⇑e ⋯ ⋯ ⋯

noncomputable instance Equiv.instMulZeroClassShrink {α : Type u} [Small.{v, u} α] [MulZeroClass α] : MulZeroClass (Shrink.{v, u} α)

Equations

• Equiv.instMulZeroClassShrink = Equiv.mulZeroClass (equivShrink α).symm

theorem Equiv.addZeroClass.proof_2 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddZeroClass β] : ∀ (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 : α ≃ β) [AddZeroClass β] : e (e.symm 0) = 0

@[reducible]

def Equiv.addZeroClass {α : Type u} {β : Type v} (e : α ≃ β) [AddZeroClass β] : AddZeroClass α

Transfer AddZeroClass across an Equiv

Equations

• Equiv.addZeroClass e = let one := Equiv.zero e; let mul := Equiv.add e; Function.Injective.addZeroClass ⇑e ⋯ ⋯ ⋯

@[reducible]

def Equiv.mulOneClass {α : Type u} {β : Type v} (e : α ≃ β) [MulOneClass β] : MulOneClass α

Transfer MulOneClass across an Equiv

Equations

• Equiv.mulOneClass e = let one := Equiv.one e; let mul := Equiv.mul e; Function.Injective.mulOneClass ⇑e ⋯ ⋯ ⋯

noncomputable instance Equiv.instAddZeroClassShrink {α : Type u} [Small.{v, u} α] [AddZeroClass α] : AddZeroClass (Shrink.{v, u} α)

Equations

• Equiv.instAddZeroClassShrink = Equiv.addZeroClass (equivShrink α).symm

noncomputable instance Equiv.instMulOneClassShrink {α : Type u} [Small.{v, u} α] [MulOneClass α] : MulOneClass (Shrink.{v, u} α)

Equations

• Equiv.instMulOneClassShrink = Equiv.mulOneClass (equivShrink α).symm

@[reducible]

def Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroOneClass β] : MulZeroOneClass α

Transfer MulZeroOneClass across an Equiv

Equations

• Equiv.mulZeroOneClass e = let zero := Equiv.zero e; let one := Equiv.one e; let mul := Equiv.mul e; Function.Injective.mulZeroOneClass ⇑e ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instMulZeroOneClassShrink {α : Type u} [Small.{v, u} α] [MulZeroOneClass α] : MulZeroOneClass (Shrink.{v, u} α)

Equations

• Equiv.instMulZeroOneClassShrink = Equiv.mulZeroOneClass (equivShrink α).symm

theorem Equiv.addMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddMonoid β] : ∀ (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 : α ≃ β) [AddMonoid β] : e (e.symm 0) = 0

@[reducible]

def Equiv.addMonoid {α : Type u} {β : Type v} (e : α ≃ β) [AddMonoid β] : AddMonoid α

Transfer AddMonoid across an Equiv

Equations

• Equiv.addMonoid e = let one := Equiv.zero e; let mul := Equiv.add e; let pow := Equiv.smul e ℕ; Function.Injective.addMonoid ⇑e ⋯ ⋯ ⋯ ⋯

theorem Equiv.addMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddMonoid β] : ∀ (x : α) (n : ℕ), e (e.symm (n • e x)) = n • e x

@[reducible]

def Equiv.monoid {α : Type u} {β : Type v} (e : α ≃ β) [Monoid β] : Monoid α

Transfer Monoid across an Equiv

Equations

• Equiv.monoid e = let one := Equiv.one e; let mul := Equiv.mul e; let pow := Equiv.pow e ℕ; Function.Injective.monoid ⇑e ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instAddMonoidShrink {α : Type u} [Small.{v, u} α] [AddMonoid α] : AddMonoid (Shrink.{v, u} α)

Equations

• Equiv.instAddMonoidShrink = Equiv.addMonoid (equivShrink α).symm

noncomputable instance Equiv.instMonoidShrink {α : Type u} [Small.{v, u} α] [Monoid α] : Monoid (Shrink.{v, u} α)

Equations

• Equiv.instMonoidShrink = Equiv.monoid (equivShrink α).symm

theorem Equiv.addCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommMonoid β] : e (e.symm 0) = 0

theorem Equiv.addCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommMonoid β] : ∀ (x : α) (n : ℕ), e (e.symm (n • e x)) = n • e x

theorem Equiv.addCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommMonoid β] : ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y

@[reducible]

def Equiv.addCommMonoid {α : Type u} {β : Type v} (e : α ≃ β) [AddCommMonoid β] : AddCommMonoid α

Transfer AddCommMonoid across an Equiv

Equations

• Equiv.addCommMonoid e = let one := Equiv.zero e; let mul := Equiv.add e; let pow := Equiv.smul e ℕ; Function.Injective.addCommMonoid ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible]

def Equiv.commMonoid {α : Type u} {β : Type v} (e : α ≃ β) [CommMonoid β] : CommMonoid α

Transfer CommMonoid across an Equiv

Equations

• Equiv.commMonoid e = let one := Equiv.one e; let mul := Equiv.mul e; let pow := Equiv.pow e ℕ; Function.Injective.commMonoid ⇑e ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instAddCommMonoidShrink {α : Type u} [Small.{v, u} α] [AddCommMonoid α] : AddCommMonoid (Shrink.{v, u} α)

Equations

• Equiv.instAddCommMonoidShrink = Equiv.addCommMonoid (equivShrink α).symm

noncomputable instance Equiv.instCommMonoidShrink {α : Type u} [Small.{v, u} α] [CommMonoid α] : CommMonoid (Shrink.{v, u} α)

Equations

• Equiv.instCommMonoidShrink = Equiv.commMonoid (equivShrink α).symm

theorem Equiv.addGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddGroup β] : ∀ (x : α) (n : ℕ), e (e.symm (n • e x)) = n • e x

theorem Equiv.addGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddGroup β] : e (e.symm 0) = 0

@[reducible]

def Equiv.addGroup {α : Type u} {β : Type v} (e : α ≃ β) [AddGroup β] : AddGroup α

Transfer AddGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

theorem Equiv.addGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddGroup β] : ∀ (x : α) (n : ℤ), e (e.symm (n • e x)) = n • e x

theorem Equiv.addGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddGroup β] : ∀ (x : α), e (e.symm (-e x)) = -e x

theorem Equiv.addGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddGroup β] : ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y

theorem Equiv.addGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddGroup β] : ∀ (x y : α), e (e.symm (e x - e y)) = e x - e y

@[reducible]

def Equiv.group {α : Type u} {β : Type v} (e : α ≃ β) [Group β] : Group α

Transfer Group across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instAddGroupShrink {α : Type u} [Small.{v, u} α] [AddGroup α] : AddGroup (Shrink.{v, u} α)

Equations

• Equiv.instAddGroupShrink = Equiv.addGroup (equivShrink α).symm

noncomputable instance Equiv.instGroupShrink {α : Type u} [Small.{v, u} α] [Group α] : Group (Shrink.{v, u} α)

Equations

• Equiv.instGroupShrink = Equiv.group (equivShrink α).symm

theorem Equiv.addCommGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommGroup β] : ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y

theorem Equiv.addCommGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommGroup β] : e (e.symm 0) = 0

theorem Equiv.addCommGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommGroup β] : ∀ (x : α) (n : ℤ), e (e.symm (n • e x)) = n • e x

theorem Equiv.addCommGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommGroup β] : ∀ (x : α), e (e.symm (-e x)) = -e x

theorem Equiv.addCommGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommGroup β] : ∀ (x : α) (n : ℕ), e (e.symm (n • e x)) = n • e x

theorem Equiv.addCommGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α ≃ β) [AddCommGroup β] : ∀ (x y : α), e (e.symm (e x - e y)) = e x - e y

@[reducible]

def Equiv.addCommGroup {α : Type u} {β : Type v} (e : α ≃ β) [AddCommGroup β] : AddCommGroup α

Transfer AddCommGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Equiv.commGroup {α : Type u} {β : Type v} (e : α ≃ β) [CommGroup β] : CommGroup α

Transfer CommGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instAddCommGroupShrink {α : Type u} [Small.{v, u} α] [AddCommGroup α] : AddCommGroup (Shrink.{v, u} α)

Equations

• Equiv.instAddCommGroupShrink = Equiv.addCommGroup (equivShrink α).symm

noncomputable instance Equiv.instCommGroupShrink {α : Type u} [Small.{v, u} α] [CommGroup α] : CommGroup (Shrink.{v, u} α)

Equations

• Equiv.instCommGroupShrink = Equiv.commGroup (equivShrink α).symm

@[reducible]

def Equiv.nonUnitalNonAssocSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring α

Transfer NonUnitalNonAssocSemiring across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instNonUnitalNonAssocSemiringShrink {α : Type u} [Small.{v, u} α] [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalNonAssocSemiringShrink = Equiv.nonUnitalNonAssocSemiring (equivShrink α).symm

@[reducible]

def Equiv.nonUnitalSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalSemiring β] : NonUnitalSemiring α

Transfer NonUnitalSemiring across an Equiv

Equations

• Equiv.nonUnitalSemiring e = let zero := Equiv.zero e; let add := Equiv.add e; let mul := Equiv.mul e; let nsmul := Equiv.smul e ℕ; Function.Injective.nonUnitalSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instNonUnitalSemiringShrink {α : Type u} [Small.{v, u} α] [NonUnitalSemiring α] : NonUnitalSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalSemiringShrink = Equiv.nonUnitalSemiring (equivShrink α).symm

@[reducible]

def Equiv.addMonoidWithOne {α : Type u} {β : Type v} (e : α ≃ β) [AddMonoidWithOne β] : AddMonoidWithOne α

Transfer AddMonoidWithOne across an Equiv

Equations

• Equiv.addMonoidWithOne e = let __src := Equiv.addMonoid e; let __src_1 := Equiv.one e; AddMonoidWithOne.mk ⋯ ⋯

noncomputable instance Equiv.instAddMonoidWithOneShrink {α : Type u} [Small.{v, u} α] [AddMonoidWithOne α] : AddMonoidWithOne (Shrink.{v, u} α)

Equations

• Equiv.instAddMonoidWithOneShrink = Equiv.addMonoidWithOne (equivShrink α).symm

@[reducible]

def Equiv.addGroupWithOne {α : Type u} {β : Type v} (e : α ≃ β) [AddGroupWithOne β] : AddGroupWithOne α

Transfer AddGroupWithOne across an Equiv

Equations

• Equiv.addGroupWithOne e = let __src := Equiv.addMonoidWithOne e; let __src_1 := Equiv.addGroup e; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instAddGroupWithOneShrink {α : Type u} [Small.{v, u} α] [AddGroupWithOne α] : AddGroupWithOne (Shrink.{v, u} α)

Equations

• Equiv.instAddGroupWithOneShrink = Equiv.addGroupWithOne (equivShrink α).symm

@[reducible]

def Equiv.nonAssocSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonAssocSemiring β] : NonAssocSemiring α

Transfer NonAssocSemiring across an Equiv

Equations

• Equiv.nonAssocSemiring e = let mul := Equiv.mul e; let add_monoid_with_one := Equiv.addMonoidWithOne e; Function.Injective.nonAssocSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instNonAssocSemiringShrink {α : Type u} [Small.{v, u} α] [NonAssocSemiring α] : NonAssocSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonAssocSemiringShrink = Equiv.nonAssocSemiring (equivShrink α).symm

@[reducible]

def Equiv.semiring {α : Type u} {β : Type v} (e : α ≃ β) [Semiring β] : Semiring α

Transfer Semiring across an Equiv

Equations

• Equiv.semiring e = let mul := Equiv.mul e; let add_monoid_with_one := Equiv.addMonoidWithOne e; let npow := Equiv.pow e ℕ; Function.Injective.semiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instSemiringShrink {α : Type u} [Small.{v, u} α] [Semiring α] : Semiring (Shrink.{v, u} α)

Equations

• Equiv.instSemiringShrink = Equiv.semiring (equivShrink α).symm

@[reducible]

def Equiv.nonUnitalCommSemiring {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalCommSemiring β] : NonUnitalCommSemiring α

Transfer NonUnitalCommSemiring across an Equiv

Equations

• Equiv.nonUnitalCommSemiring e = let zero := Equiv.zero e; let add := Equiv.add e; let mul := Equiv.mul e; let nsmul := Equiv.smul e ℕ; Function.Injective.nonUnitalCommSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instNonUnitalCommSemiringShrink {α : Type u} [Small.{v, u} α] [NonUnitalCommSemiring α] : NonUnitalCommSemiring (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalCommSemiringShrink = Equiv.nonUnitalCommSemiring (equivShrink α).symm

@[reducible]

def Equiv.commSemiring {α : Type u} {β : Type v} (e : α ≃ β) [CommSemiring β] : CommSemiring α

Transfer CommSemiring across an Equiv

Equations

• Equiv.commSemiring e = let mul := Equiv.mul e; let add_monoid_with_one := Equiv.addMonoidWithOne e; let npow := Equiv.pow e ℕ; Function.Injective.commSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instCommSemiringShrink {α : Type u} [Small.{v, u} α] [CommSemiring α] : CommSemiring (Shrink.{v, u} α)

Equations

• Equiv.instCommSemiringShrink = Equiv.commSemiring (equivShrink α).symm

@[reducible]

def Equiv.nonUnitalNonAssocRing {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α

Transfer NonUnitalNonAssocRing across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instNonUnitalNonAssocRingShrink {α : Type u} [Small.{v, u} α] [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalNonAssocRingShrink = Equiv.nonUnitalNonAssocRing (equivShrink α).symm

@[reducible]

def Equiv.nonUnitalRing {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalRing β] : NonUnitalRing α

Transfer NonUnitalRing across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instNonUnitalRingShrink {α : Type u} [Small.{v, u} α] [NonUnitalRing α] : NonUnitalRing (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalRingShrink = Equiv.nonUnitalRing (equivShrink α).symm

@[reducible]

def Equiv.nonAssocRing {α : Type u} {β : Type v} (e : α ≃ β) [NonAssocRing β] : NonAssocRing α

Transfer NonAssocRing across an Equiv

Equations

• Equiv.nonAssocRing e = let add_group_with_one := Equiv.addGroupWithOne e; let mul := Equiv.mul e; Function.Injective.nonAssocRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instNonAssocRingShrink {α : Type u} [Small.{v, u} α] [NonAssocRing α] : NonAssocRing (Shrink.{v, u} α)

Equations

• Equiv.instNonAssocRingShrink = Equiv.nonAssocRing (equivShrink α).symm

@[reducible]

def Equiv.ring {α : Type u} {β : Type v} (e : α ≃ β) [Ring β] : Ring α

Transfer Ring across an Equiv

Equations

• Equiv.ring e = let mul := Equiv.mul e; let add_group_with_one := Equiv.addGroupWithOne e; let npow := Equiv.pow e ℕ; Function.Injective.ring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instRingShrink {α : Type u} [Small.{v, u} α] [Ring α] : Ring (Shrink.{v, u} α)

Equations

• Equiv.instRingShrink = Equiv.ring (equivShrink α).symm

@[reducible]

def Equiv.nonUnitalCommRing {α : Type u} {β : Type v} (e : α ≃ β) [NonUnitalCommRing β] : NonUnitalCommRing α

Transfer NonUnitalCommRing across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instNonUnitalCommRingShrink {α : Type u} [Small.{v, u} α] [NonUnitalCommRing α] : NonUnitalCommRing (Shrink.{v, u} α)

Equations

• Equiv.instNonUnitalCommRingShrink = Equiv.nonUnitalCommRing (equivShrink α).symm

@[reducible]

def Equiv.commRing {α : Type u} {β : Type v} (e : α ≃ β) [CommRing β] : CommRing α

Transfer CommRing across an Equiv

Equations

• Equiv.commRing e = let mul := Equiv.mul e; let add_group_with_one := Equiv.addGroupWithOne e; let npow := Equiv.pow e ℕ; Function.Injective.commRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Equiv.instCommRingShrink {α : Type u} [Small.{v, u} α] [CommRing α] : CommRing (Shrink.{v, u} α)

Equations

• Equiv.instCommRingShrink = Equiv.commRing (equivShrink α).symm

@[reducible]

theorem Equiv.nontrivial {α : Type u} {β : Type v} (e : α ≃ β) [Nontrivial β] : Nontrivial α

Transfer Nontrivial across an Equiv

noncomputable instance Equiv.instNontrivialShrink {α : Type u} [Small.{v, u} α] [Nontrivial α] : Nontrivial (Shrink.{v, u} α)

Equations

• ⋯ = ⋯

@[reducible]

theorem Equiv.isDomain {α : Type u} {β : Type v} [Ring α] [Ring β] [IsDomain β] (e : α ≃+* β) : IsDomain α

Transfer IsDomain across an Equiv

noncomputable instance Equiv.instIsDomainShrinkInstSemiringShrinkToSemiring {α : Type u} [Small.{v, u} α] [Ring α] [IsDomain α] : IsDomain (Shrink.{v, u} α)

Equations

• ⋯ = ⋯

@[reducible]

def Equiv.RatCast {α : Type u} {β : Type v} (e : α ≃ β) [RatCast β] : RatCast α

Transfer RatCast across an Equiv

Equations

• Equiv.RatCast e = { ratCast := fun (n : ℚ) => e.symm ↑n }

noncomputable instance Equiv.instRatCastShrink {α : Type u} [Small.{v, u} α] [RatCast α] : RatCast (Shrink.{v, u} α)

Equations

• Equiv.instRatCastShrink = Equiv.RatCast (equivShrink α).symm

@[reducible]

def Equiv.divisionRing {α : Type u} {β : Type v} (e : α ≃ β) [DivisionRing β] : DivisionRing α

Transfer DivisionRing across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instDivisionRingShrink {α : Type u} [Small.{v, u} α] [DivisionRing α] : DivisionRing (Shrink.{v, u} α)

Equations

• Equiv.instDivisionRingShrink = Equiv.divisionRing (equivShrink α).symm

@[reducible]

def Equiv.field {α : Type u} {β : Type v} (e : α ≃ β) [Field β] : Field α

Transfer Field across an Equiv

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Equiv.instFieldShrink {α : Type u} [Small.{v, u} α] [Field α] : Field (Shrink.{v, u} α)

Equations

• Equiv.instFieldShrink = Equiv.field (equivShrink α).symm

@[reducible]

def Equiv.mulAction {α : Type u} {β : Type v} (R : Type u_1) [Monoid R] (e : α ≃ β) [MulAction R β] : MulAction R α

Transfer MulAction across an Equiv

Equations

• Equiv.mulAction R e = let __src := Equiv.smul e R; MulAction.mk ⋯ ⋯

noncomputable instance Equiv.instMulActionShrink {α : Type u} (R : Type u_1) [Monoid R] [Small.{v, u} α] [MulAction R α] : MulAction R (Shrink.{v, u} α)

Equations

• Equiv.instMulActionShrink R = Equiv.mulAction R (equivShrink α).symm

@[reducible]

def Equiv.distribMulAction {α : Type u} {β : Type v} (R : Type u_1) [Monoid R] (e : α ≃ β) [AddCommMonoid β] [DistribMulAction R β] : DistribMulAction R α

Transfer DistribMulAction across an Equiv

Equations

• Equiv.distribMulAction R e = let __src := Equiv.mulAction R e; DistribMulAction.mk ⋯ ⋯

noncomputable instance Equiv.instDistribMulActionShrinkInstAddMonoidShrinkToAddMonoid {α : Type u} (R : Type u_1) [Monoid R] [Small.{v, u} α] [AddCommMonoid α] [DistribMulAction R α] : DistribMulAction R (Shrink.{v, u} α)

Equations

• Equiv.instDistribMulActionShrinkInstAddMonoidShrinkToAddMonoid R = Equiv.distribMulAction R (equivShrink α).symm

@[reducible]

def Equiv.module {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α ≃ β) [AddCommMonoid β] : let addCommMonoid := Equiv.addCommMonoid e; [inst : Module R β] → Module R α

Transfer Module across an Equiv

Equations

• @Equiv.module α β R inst✝ e inst = let addCommMonoid := Equiv.addCommMonoid e; fun [Module R β] => let __src := Equiv.distribMulAction R e; Module.mk ⋯ ⋯

noncomputable instance Equiv.instModuleShrinkInstAddCommMonoidShrink {α : Type u} (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] : Module R (Shrink.{v, u} α)

Equations

• Equiv.instModuleShrinkInstAddCommMonoidShrink R = Equiv.module R (equivShrink α).symm

def Equiv.linearEquiv {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α ≃ β) [AddCommMonoid β] [Module R β] : let addCommMonoid := Equiv.addCommMonoid e; let module := Equiv.module R e; α ≃ₗ[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.

@[simp]

theorem Shrink.linearEquiv_symm_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] : ∀ (a : α), (LinearEquiv.symm (Shrink.linearEquiv α R)) a = (AddEquiv.symm (Equiv.addEquiv (equivShrink α).symm)) a

@[simp]

theorem Shrink.linearEquiv_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] : ∀ (a : Shrink.{v, u} α), (Shrink.linearEquiv α R) a = (equivShrink α).symm a

noncomputable def Shrink.linearEquiv (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] : Shrink.{v, u} α ≃ₗ[R] α

Shrink α to a smaller universe preserves module structure.

Equations

• Shrink.linearEquiv α R = Equiv.linearEquiv R (equivShrink α).symm

@[reducible]

def Equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] : let semiring := Equiv.semiring e; [inst : Algebra R β] → Algebra R α

Transfer Algebra across an Equiv

Equations

• @Equiv.algebra α β R inst✝ e inst = let semiring := Equiv.semiring e; fun [Algebra R β] => Algebra.ofModule ⋯ ⋯

theorem Equiv.algebraMap_def {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) : let semiring := Equiv.semiring e; let algebra := Equiv.algebra R e; (algebraMap R α) r = e.symm ((algebraMap R β) r)

noncomputable instance Equiv.instAlgebraShrinkInstSemiringShrink {α : Type u} (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] : Algebra R (Shrink.{v, u} α)

Equations

• Equiv.instAlgebraShrinkInstSemiringShrink R = Equiv.algebra R (equivShrink α).symm

def Equiv.algEquiv {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] : let semiring := Equiv.semiring e; let algebra := Equiv.algebra R e; α ≃ₐ[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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Equiv.algEquiv_apply {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (Equiv.algEquiv R e) a = e a

theorem Equiv.algEquiv_symm_apply {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) : (AlgEquiv.symm (Equiv.algEquiv R e)) b = e.symm b

@[simp]

theorem Shrink.algEquiv_apply (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] : ∀ (a : Shrink.{v, u} α), (Shrink.algEquiv α R) a = (equivShrink α).symm a

@[simp]

theorem Shrink.algEquiv_symm_apply (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] : ∀ (a : α), (AlgEquiv.symm (Shrink.algEquiv α R)) a = (equivShrink α) a

noncomputable def Shrink.algEquiv (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] : Shrink.{v, u} α ≃ₐ[R] α

Shrink α to a smaller universe preserves algebra structure.

Equations

• Shrink.algEquiv α R = Equiv.algEquiv R (equivShrink α).symm

theorem Finite.exists_type_zero_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] : ∃ (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.