Multiplicative and additive equivs #

In this file we define two extensions of Equiv called AddEquiv and MulEquiv, which are datatypes representing isomorphisms of AddMonoids/AddGroups and Monoids/Groups.

Notations #

infix ` ≃* `:25 := MulEquiv≃* `:25 := MulEquiv
infix ` ≃+ `:25 := AddEquiv≃+ `:25 := AddEquiv

The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.

Tags #

Equiv, MulEquiv, AddEquiv

source

ink

def AddHom.inverse {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : N → M) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) :

AddHom N M

Makes an additive inverse from a bijection which preserves addition.

Equations

AddHom.inverse f g h₁ h₂ = { toFun := g, map_add' := (_ : ∀ (x y : N), g (x + y) = g x + g y) }

source

ink

def AddHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : N → M) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) (x : N) (y : N) :

g (x + y) = g x + g y

Equations

(_ : g (x + y) = g x + g y) = (_ : g (x + y) = g x + g y)

source

ink

def MulHom.inverse {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) :

N →ₙ* M

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations

MulHom.inverse f g h₁ h₂ = { toFun := g, map_mul' := (_ : ∀ (x y : N), g (x * y) = g x * g y) }

source

ink

def AddMonoidHom.inverse.proof_2 {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) (x : B) (y : B) :

AddHom.toFun (AddHom.inverse (↑f) g h₁ h₂) (x + y) = AddHom.toFun (AddHom.inverse (↑f) g h₁ h₂) x + AddHom.toFun (AddHom.inverse (↑f) g h₁ h₂) y

Equations

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

source

ink

def AddMonoidHom.inverse.proof_1 {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ↑f) :

g 0 = 0

Equations

(_ : g 0 = 0) = (_ : g 0 = 0)

source

ink

def AddMonoidHom.inverse {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) :

B →+ A

The inverse of a bijective AddMonoidHom is an AddMonoidHom.

Equations

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

source

ink

@[simp]

theorem MonoidHom.inverse_apply {A : Type u_1} {B : Type u_2} [inst : Monoid A] [inst : Monoid B] (f : A →* B) (g : B → A) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) :

∀ (a : B), ↑(MonoidHom.inverse f g h₁ h₂) a = g a

source

ink

@[simp]

theorem AddMonoidHom.inverse_apply {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) :

∀ (a : B), ↑(AddMonoidHom.inverse f g h₁ h₂) a = g a

source

ink

def MonoidHom.inverse {A : Type u_1} {B : Type u_2} [inst : Monoid A] [inst : Monoid B] (f : A →* B) (g : B → A) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) :

B →* A

The inverse of a bijective MonoidHom is a MonoidHom.

Equations

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

source

ink

structure AddEquiv (A : Type u_1) (B : Type u_2) [inst : Add A] [inst : Add B] extends Equiv :

Type (maxu_1u_2)

The proposition that the function preserves addition
map_add' : ∀ (x y : A), Equiv.toFun toEquiv (x + y) = Equiv.toFun toEquiv x + Equiv.toFun toEquiv y

AddEquiv α β is the type of an equiv α ≃ β≃ β which preserves addition.

Instances For

source

ink

class AddEquivClass (F : Type u_1) (A : outParam (Type u_2)) (B : outParam (Type u_3)) [inst : Add A] [inst : Add B] extends EquivLike :

Type (max(maxu_1u_2)u_3)

Preserves addition.
map_add : ∀ (f : F) (a b : A), ↑f (a + b) = ↑f a + ↑f b

AddEquivClass F A B states that F is a type of addition-preserving morphisms. You should extend this class when you extend AddEquiv.

Instances

source

ink

abbrev AddEquiv.toAddHom {A : Type u_1} {B : Type u_2} [inst : Add A] [inst : Add B] (self : A ≃+ B) :

AddHom A B

The AddHom underlying a AddEquiv.

Equations

AddEquiv.toAddHom self = { toFun := self.toEquiv.toFun, map_add' := (_ : ∀ (x y : A), Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y) }

source

ink

structure MulEquiv (M : Type u_1) (N : Type u_2) [inst : Mul M] [inst : Mul N] extends Equiv :

Type (maxu_1u_2)

The proposition that the function preserves multiplication
map_mul' : ∀ (x y : M), Equiv.toFun toEquiv (x * y) = Equiv.toFun toEquiv x * Equiv.toFun toEquiv y

MulEquiv α β is the type of an equiv α ≃ β≃ β which preserves multiplication.

Instances For

source

ink

abbrev MulEquiv.toMulHom {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (self : M ≃* N) :

M →ₙ* N

The MulHom underlying a MulEquiv.

Equations

MulEquiv.toMulHom self = { toFun := self.toEquiv.toFun, map_mul' := (_ : ∀ (x y : M), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y) }

source

ink

class MulEquivClass (F : Type u_1) (A : outParam (Type u_2)) (B : outParam (Type u_3)) [inst : Mul A] [inst : Mul B] extends EquivLike :

Type (max(maxu_1u_2)u_3)

Preserves multiplication.
map_mul : ∀ (f : F) (a b : A), ↑f (a * b) = ↑f a * ↑f b

MulEquivClass F A B states that F is a type of multiplication-preserving morphisms. You should extend this class when you extend MulEquiv.

Instances

source

ink

def «term_≃*_» :

Lean.TrailingParserDescr

Notation for a MulEquiv.

Equations

«term_≃*_» = Lean.ParserDescr.trailingNode `term_≃*_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃* ") (Lean.ParserDescr.cat `term 26))

source

ink

def «term_≃+_» :

Lean.TrailingParserDescr

Notation for an AddEquiv.

Equations

«term_≃+_» = Lean.ParserDescr.trailingNode `term_≃+_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+ ") (Lean.ParserDescr.cat `term 26))

source

ink

instance AddEquivClass.instAddHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :

{x : Add M} → {x_1 : Add N} → [h : AddEquivClass F M N] → AddHomClass F M N

Equations

AddEquivClass.instAddHomClass F = AddHomClass.mk (_ : ∀ (f : F) (a b : M), ↑f (a + b) = ↑f a + ↑f b)

source

ink

def AddEquivClass.instAddHomClass.proof_1 (F : Type u_1) {M : Type u_2} {N : Type u_3} :

∀ {x : Add M} {x_1 : Add N} [h : AddEquivClass F M N], Function.Injective FunLike.coe

Equations

(_ : Function.Injective FunLike.coe) = (_ : Function.Injective FunLike.coe)

source

ink

instance MulEquivClass.instMulHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :

{x : Mul M} → {x_1 : Mul N} → [h : MulEquivClass F M N] → MulHomClass F M N

Equations

MulEquivClass.instMulHomClass F = MulHomClass.mk (_ : ∀ (f : F) (a b : M), ↑f (a * b) = ↑f a * ↑f b)

source

ink

instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :

{x : AddZeroClass M} → {x_1 : AddZeroClass N} → [inst : AddEquivClass F M N] → AddMonoidHomClass F M N

Equations

AddEquivClass.instAddMonoidHomClass F = let src := AddEquivClass.instAddHomClass F; AddMonoidHomClass.mk (_ : ∀ (e : F), ↑e 0 = 0)

source

ink

def AddEquivClass.instAddMonoidHomClass.proof_2 (F : Type u_3) {M : Type u_2} {N : Type u_1} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddEquivClass F M N] (f : F) (x_2 y : M), ↑f (x_2 + y) = ↑f x_2 + ↑f y

Equations

(_ : ∀ (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y) = (_ : ∀ (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y)

source

ink

def AddEquivClass.instAddMonoidHomClass.proof_1 (F : Type u_1) {M : Type u_2} {N : Type u_3} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddEquivClass F M N], Function.Injective FunLike.coe

Equations

(_ : Function.Injective FunLike.coe) = (_ : Function.Injective FunLike.coe)

source

ink

def AddEquivClass.instAddMonoidHomClass.proof_3 (F : Type u_2) {M : Type u_3} {N : Type u_1} :

∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddEquivClass F M N] (e : F), ↑e 0 = 0

Equations

(_ : ↑e 0 = 0) = (_ : ↑e 0 = 0)

source

ink

instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :

{x : MulOneClass M} → {x_1 : MulOneClass N} → [inst : MulEquivClass F M N] → MonoidHomClass F M N

Equations

MulEquivClass.instMonoidHomClass F = let src := MulEquivClass.instMulHomClass F; MonoidHomClass.mk (_ : ∀ (e : F), ↑e 1 = 1)

source

ink

instance MulEquivClass.toMonoidWithZeroHomClass (F : Type u_1) {α : Type u_2} {β : Type u_3} :

{x : MulZeroOneClass α} → {x_1 : MulZeroOneClass β} → [inst : MulEquivClass F α β] → MonoidWithZeroHomClass F α β

Equations

MulEquivClass.toMonoidWithZeroHomClass F = let src := MulEquivClass.instMonoidHomClass F; MonoidWithZeroHomClass.mk (_ : ∀ (e : F), ↑e 0 = 0)

source

ink

@[simp]

theorem AddEquivClass.map_eq_zero_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddEquivClass F M N] (h : F) {x : M} :

↑h x = 0 ↔ x = 0

source

ink

@[simp]

theorem MulEquivClass.map_eq_one_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulEquivClass F M N] (h : F) {x : M} :

↑h x = 1 ↔ x = 1

source

ink

theorem AddEquivClass.map_ne_zero_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddEquivClass F M N] (h : F) {x : M} :

↑h x ≠ 0 ↔ x ≠ 0

source

ink

theorem MulEquivClass.map_ne_one_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulEquivClass F M N] (h : F) {x : M} :

↑h x ≠ 1 ↔ x ≠ 1

source

ink

def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst : Add β] [inst : AddEquivClass F α β] (f : F) :

α ≃+ β

Turn an element of a type F satisfying AddEquivClass F α β into an actual AddEquiv. This is declared as the default coercion from F to α ≃+ β≃+ β.

Equations

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

source

ink

def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst : Mul β] [inst : MulEquivClass F α β] (f : F) :

α ≃* β

Turn an element of a type F satisfying MulEquivClass F α β into an actual MulEquiv. This is declared as the default coercion from F to α ≃* β≃* β.

Equations

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

source

ink

instance instCoeTCAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst : Add β] [inst : AddEquivClass F α β] :

CoeTC F (α ≃+ β)

Any type satisfying AddEquivClass can be cast into AddEquiv via AddEquivClass.toAddEquiv.

Equations

instCoeTCAddEquiv = { coe := AddEquivClass.toAddEquiv }

source

ink

instance instCoeTCMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst : Mul β] [inst : MulEquivClass F α β] :

CoeTC F (α ≃* β)

Any type satisfying MulEquivClass can be cast into MulEquiv via MulEquivClass.toMulEquiv.

Equations

instCoeTCMulEquiv = { coe := MulEquivClass.toMulEquiv }

source

ink

def AddEquiv.instAddEquivClassAddEquiv.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) (g : M ≃+ N) (h₁ : (fun f => f.toEquiv.toFun) f = (fun f => f.toEquiv.toFun) g) (h₂ : (fun f => f.toEquiv.invFun) f = (fun f => f.toEquiv.invFun) g) :

f = g

Equations

(_ : f = g) = (_ : f = g)

source

ink

instance AddEquiv.instAddEquivClassAddEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

AddEquivClass (M ≃+ N) M N

Equations

AddEquiv.instAddEquivClassAddEquiv = AddEquivClass.mk (_ : ∀ (self : M ≃+ N) (x y : M), Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y)

source

ink

def AddEquiv.instAddEquivClassAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

Function.LeftInverse f.toEquiv.invFun f.toEquiv.toFun

Equations

(_ : Function.LeftInverse f.toEquiv.invFun f.toEquiv.toFun) = (_ : Function.LeftInverse f.toEquiv.invFun f.toEquiv.toFun)

source

ink

def AddEquiv.instAddEquivClassAddEquiv.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

Function.RightInverse f.toEquiv.invFun f.toEquiv.toFun

Equations

(_ : Function.RightInverse f.toEquiv.invFun f.toEquiv.toFun) = (_ : Function.RightInverse f.toEquiv.invFun f.toEquiv.toFun)

source

ink

instance MulEquiv.instMulEquivClassMulEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

MulEquivClass (M ≃* N) M N

Equations

MulEquiv.instMulEquivClassMulEquiv = MulEquivClass.mk (_ : ∀ (self : M ≃* N) (x y : M), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y)

source

ink

@[simp]

theorem AddEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

f.toEquiv = ↑f

source

ink

@[simp]

theorem MulEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :

f.toEquiv = ↑f

source

ink

@[simp]

theorem AddEquiv.coe_toEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

↑↑f = ↑f

source

ink

@[simp]

theorem MulEquiv.coe_toEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :

↑↑f = ↑f

source

ink

@[simp]

theorem AddEquiv.coe_toAddHom {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} :

↑(AddEquiv.toAddHom f) = ↑f

source

ink

@[simp]

theorem MulEquiv.coe_toMulHom {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} :

↑(MulEquiv.toMulHom f) = ↑f

source

ink

theorem AddEquiv.map_add {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) (x : M) (y : M) :

↑f (x + y) = ↑f x + ↑f y

An additive isomorphism preserves addition.

source

ink

theorem MulEquiv.map_mul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) (x : M) (y : M) :

↑f (x * y) = ↑f x * ↑f y

A multiplicative isomorphism preserves multiplication.

source

ink

def AddEquiv.mk' {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃ N) (h : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) :

M ≃+ N

Makes an additive isomorphism from a bijection which preserves addition.

Equations

AddEquiv.mk' f h = { toEquiv := f, map_add' := h }

source

ink

def MulEquiv.mk' {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃ N) (h : ∀ (x y : M), ↑f (x * y) = ↑f x * ↑f y) :

M ≃* N

Makes a multiplicative isomorphism from a bijection which preserves multiplication.

Equations

MulEquiv.mk' f h = { toEquiv := f, map_mul' := h }

source

ink

theorem AddEquiv.bijective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

Function.Bijective ↑e

source

ink

theorem MulEquiv.bijective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

Function.Bijective ↑e

source

ink

theorem AddEquiv.injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

Function.Injective ↑e

source

ink

theorem MulEquiv.injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

Function.Injective ↑e

source

ink

theorem AddEquiv.surjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

Function.Surjective ↑e

source

ink

theorem MulEquiv.surjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

Function.Surjective ↑e

source

ink

def AddEquiv.refl (M : Type u_1) [inst : Add M] :

M ≃+ M

The identity map is an additive isomorphism.

Equations

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

source

ink

def AddEquiv.refl.proof_1 (M : Type u_1) [inst : Add M] :

∀ (x x_1 : M), Equiv.toFun { toFun := (Equiv.refl M).toFun, invFun := (Equiv.refl M).invFun, left_inv := (_ : Function.LeftInverse (Equiv.refl M).invFun (Equiv.refl M).toFun), right_inv := (_ : Function.RightInverse (Equiv.refl M).invFun (Equiv.refl M).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.refl M).toFun, invFun := (Equiv.refl M).invFun, left_inv := (_ : Function.LeftInverse (Equiv.refl M).invFun (Equiv.refl M).toFun), right_inv := (_ : Function.RightInverse (Equiv.refl M).invFun (Equiv.refl M).toFun) } (x + x_1)

Equations

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

source

ink

def MulEquiv.refl (M : Type u_1) [inst : Mul M] :

M ≃* M

The identity map is a multiplicative isomorphism.

Equations

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

source

ink

instance AddEquiv.instInhabitedAddEquiv {M : Type u_1} [inst : Add M] :

Inhabited (M ≃+ M)

Equations

AddEquiv.instInhabitedAddEquiv = { default := AddEquiv.refl M }

source

ink

instance MulEquiv.instInhabitedMulEquiv {M : Type u_1} [inst : Mul M] :

Inhabited (M ≃* M)

Equations

MulEquiv.instInhabitedMulEquiv = { default := MulEquiv.refl M }

source

ink

def AddEquiv.symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (h : M ≃+ N) :

N ≃+ M

The inverse of an isomorphism is an isomorphism.

Equations

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

source

ink

def AddEquiv.symm.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (h : M ≃+ N) (a : N) (b : N) :

↑(AddHom.inverse (AddEquiv.toAddHom h) ↑(Equiv.symm h.toEquiv) (_ : Function.LeftInverse h.toEquiv.invFun h.toEquiv.toFun) (_ : Function.RightInverse h.toEquiv.invFun h.toEquiv.toFun)) (a + b) = ↑(AddHom.inverse (AddEquiv.toAddHom h) ↑(Equiv.symm h.toEquiv) (_ : Function.LeftInverse h.toEquiv.invFun h.toEquiv.toFun) (_ : Function.RightInverse h.toEquiv.invFun h.toEquiv.toFun)) a + ↑(AddHom.inverse (AddEquiv.toAddHom h) ↑(Equiv.symm h.toEquiv) (_ : Function.LeftInverse h.toEquiv.invFun h.toEquiv.toFun) (_ : Function.RightInverse h.toEquiv.invFun h.toEquiv.toFun)) b

Equations

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

source

ink

def MulEquiv.symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (h : M ≃* N) :

N ≃* M

The inverse of an isomorphism is an isomorphism.

Equations

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

source

ink

theorem AddEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} :

f.toEquiv.invFun = ↑(AddEquiv.symm f)

source

ink

theorem MulEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} :

f.toEquiv.invFun = ↑(MulEquiv.symm f)

source

ink

@[simp]

theorem AddEquiv.coe_toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

↑(Equiv.symm ↑f) = ↑(AddEquiv.symm f)

source

ink

@[simp]

theorem MulEquiv.coe_toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :

↑(Equiv.symm ↑f) = ↑(MulEquiv.symm f)

source

ink

@[simp]

theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

EquivLike.inv f = ↑(AddEquiv.symm f)

source

ink

@[simp]

theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :

EquivLike.inv f = ↑(MulEquiv.symm f)

source

ink

def AddEquiv.Simps.symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

N → M

See Note [custom simps projection]

Equations

AddEquiv.Simps.symm_apply e = ↑(AddEquiv.symm e)

source

ink

def MulEquiv.Simps.symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

N → M

See Note [custom simps projection]

Equations

MulEquiv.Simps.symm_apply e = ↑(MulEquiv.symm e)

source

ink

@[simp]

theorem AddEquiv.toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

↑(AddEquiv.symm f) = Equiv.symm ↑f

source

ink

@[simp]

theorem MulEquiv.toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :

↑(MulEquiv.symm f) = Equiv.symm ↑f

source

ink

@[simp]

theorem AddEquiv.coe_mk {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃ N) (hf : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) :

↑{ toEquiv := f, map_add' := hf } = ↑f

source

ink

@[simp]

theorem MulEquiv.coe_mk {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃ N) (hf : ∀ (x y : M), ↑f (x * y) = ↑f x * ↑f y) :

↑{ toEquiv := f, map_mul' := hf } = ↑f

source

ink

@[simp]

theorem AddEquiv.symm_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :

AddEquiv.symm (AddEquiv.symm f) = f

source

ink

@[simp]

theorem MulEquiv.symm_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :

MulEquiv.symm (MulEquiv.symm f) = f

source

ink

theorem AddEquiv.symm_bijective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

Function.Bijective AddEquiv.symm

source

ink

theorem MulEquiv.symm_bijective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

Function.Bijective MulEquiv.symm

source

ink

@[simp]

theorem AddEquiv.symm_mk {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃ N) (h : ∀ (x y : M), Equiv.toFun f (x + y) = Equiv.toFun f x + Equiv.toFun f y) :

AddEquiv.symm { toEquiv := f, map_add' := h } = { toEquiv := Equiv.symm f, map_add' := (_ : ∀ (x y : N), Equiv.toFun (AddEquiv.symm { toEquiv := f, map_add' := h }).toEquiv (x + y) = Equiv.toFun (AddEquiv.symm { toEquiv := f, map_add' := h }).toEquiv x + Equiv.toFun (AddEquiv.symm { toEquiv := f, map_add' := h }).toEquiv y) }

source

ink

@[simp]

theorem MulEquiv.symm_mk {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃ N) (h : ∀ (x y : M), Equiv.toFun f (x * y) = Equiv.toFun f x * Equiv.toFun f y) :

MulEquiv.symm { toEquiv := f, map_mul' := h } = { toEquiv := Equiv.symm f, map_mul' := (_ : ∀ (x y : N), Equiv.toFun (MulEquiv.symm { toEquiv := f, map_mul' := h }).toEquiv (x * y) = Equiv.toFun (MulEquiv.symm { toEquiv := f, map_mul' := h }).toEquiv x * Equiv.toFun (MulEquiv.symm { toEquiv := f, map_mul' := h }).toEquiv y) }

source

ink

@[simp]

theorem AddEquiv.refl_symm {M : Type u_1} [inst : Add M] :

AddEquiv.symm (AddEquiv.refl M) = AddEquiv.refl M

source

ink

@[simp]

theorem MulEquiv.refl_symm {M : Type u_1} [inst : Mul M] :

MulEquiv.symm (MulEquiv.refl M) = MulEquiv.refl M

source

ink

def AddEquiv.trans.proof_1 {M : Type u_2} {N : Type u_3} {P : Type u_1} [inst : Add M] [inst : Add N] [inst : Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) (x : M) (y : M) :

↑h2 (↑h1 (x + y)) = ↑h2 (↑h1 x) + ↑h2 (↑h1 y)

Equations

(_ : ↑h2 (↑h1 (x + y)) = ↑h2 (↑h1 x) + ↑h2 (↑h1 y)) = (_ : ↑h2 (↑h1 (x + y)) = ↑h2 (↑h1 x) + ↑h2 (↑h1 y))

source

ink

def AddEquiv.trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :

M ≃+ P

Transitivity of addition-preserving isomorphisms

Equations

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

source

ink

def MulEquiv.trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :

M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations

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

source

ink

@[simp]

theorem AddEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (y : N) :

↑e (↑(AddEquiv.symm e) y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

source

ink

@[simp]

theorem MulEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (y : N) :

↑e (↑(MulEquiv.symm e) y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

source

ink

@[simp]

theorem AddEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (x : M) :

↑(AddEquiv.symm e) (↑e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

source

ink

@[simp]

theorem MulEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (x : M) :

↑(MulEquiv.symm e) (↑e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

source

ink

@[simp]

theorem AddEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

↑(AddEquiv.symm e) ∘ ↑e = id

source

ink

@[simp]

theorem MulEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

↑(MulEquiv.symm e) ∘ ↑e = id

source

ink

@[simp]

theorem AddEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

↑e ∘ ↑(AddEquiv.symm e) = id

source

ink

@[simp]

theorem MulEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

↑e ∘ ↑(MulEquiv.symm e) = id

source

ink

@[simp]

theorem AddEquiv.coe_refl {M : Type u_1} [inst : Add M] :

↑(AddEquiv.refl M) = id

source

ink

@[simp]

theorem MulEquiv.coe_refl {M : Type u_1} [inst : Mul M] :

↑(MulEquiv.refl M) = id

source

ink

@[simp]

theorem AddEquiv.refl_apply {M : Type u_1} [inst : Add M] (m : M) :

↑(AddEquiv.refl M) m = m

source

ink

@[simp]

theorem MulEquiv.refl_apply {M : Type u_1} [inst : Mul M] (m : M) :

↑(MulEquiv.refl M) m = m

source

ink

@[simp]

theorem AddEquiv.coe_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :

↑(AddEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁

source

ink

@[simp]

theorem MulEquiv.coe_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :

↑(MulEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁

source

ink

@[simp]

theorem AddEquiv.trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :

↑(AddEquiv.trans e₁ e₂) m = ↑e₂ (↑e₁ m)

source

ink

@[simp]

theorem MulEquiv.trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :

↑(MulEquiv.trans e₁ e₂) m = ↑e₂ (↑e₁ m)

source

ink

@[simp]

theorem AddEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :

↑(AddEquiv.symm (AddEquiv.trans e₁ e₂)) p = ↑(AddEquiv.symm e₁) (↑(AddEquiv.symm e₂) p)

source

ink

@[simp]

theorem MulEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :

↑(MulEquiv.symm (MulEquiv.trans e₁ e₂)) p = ↑(MulEquiv.symm e₁) (↑(MulEquiv.symm e₂) p)

source

ink

theorem AddEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : M} {y : M} :

↑e x = ↑e y ↔ x = y

source

ink

theorem MulEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : M} {y : M} :

↑e x = ↑e y ↔ x = y

source

ink

theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : M} {y : N} :

↑e x = y ↔ x = ↑(AddEquiv.symm e) y

source

ink

theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : M} {y : N} :

↑e x = y ↔ x = ↑(MulEquiv.symm e) y

source

ink

theorem AddEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : N} {y : M} :

↑(AddEquiv.symm e) x = y ↔ x = ↑e y

source

ink

theorem MulEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : N} {y : (fun x => M) x} :

↑(MulEquiv.symm e) x = y ↔ x = ↑e y

source

ink

theorem AddEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : N} {y : M} :

y = ↑(AddEquiv.symm e) x ↔ ↑e y = x

source

ink

theorem MulEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : N} {y : (fun x => M) x} :

y = ↑(MulEquiv.symm e) x ↔ ↑e y = x

source

ink

theorem AddEquiv.eq_comp_symm {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : N → α) (g : M → α) :

f = g ∘ ↑(AddEquiv.symm e) ↔ f ∘ ↑e = g

source

ink

theorem MulEquiv.eq_comp_symm {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : N → α) (g : M → α) :

f = g ∘ ↑(MulEquiv.symm e) ↔ f ∘ ↑e = g

source

ink

theorem AddEquiv.comp_symm_eq {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : N → α) (g : M → α) :

g ∘ ↑(AddEquiv.symm e) = f ↔ g = f ∘ ↑e

source

ink

theorem MulEquiv.comp_symm_eq {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : N → α) (g : M → α) :

g ∘ ↑(MulEquiv.symm e) = f ↔ g = f ∘ ↑e

source

ink

theorem AddEquiv.eq_symm_comp {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : α → M) (g : α → N) :

f = ↑(AddEquiv.symm e) ∘ g ↔ ↑e ∘ f = g

source

ink

theorem MulEquiv.eq_symm_comp {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : α → M) (g : α → N) :

f = ↑(MulEquiv.symm e) ∘ g ↔ ↑e ∘ f = g

source

ink

theorem AddEquiv.symm_comp_eq {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : α → M) (g : α → N) :

↑(AddEquiv.symm e) ∘ g = f ↔ g = ↑e ∘ f

source

ink

theorem MulEquiv.symm_comp_eq {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : α → M) (g : α → N) :

↑(MulEquiv.symm e) ∘ g = f ↔ g = ↑e ∘ f

source

ink

@[simp]

theorem AddEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

AddEquiv.trans (AddEquiv.symm e) e = AddEquiv.refl N

source

ink

@[simp]

theorem MulEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

MulEquiv.trans (MulEquiv.symm e) e = MulEquiv.refl N

source

ink

@[simp]

theorem AddEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :

AddEquiv.trans e (AddEquiv.symm e) = AddEquiv.refl M

source

ink

@[simp]

theorem MulEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :

MulEquiv.trans e (MulEquiv.symm e) = MulEquiv.refl M

source

ink

theorem AddEquiv.coe_addMonoidHom_refl {M : Type u_1} [inst : AddZeroClass M] :

↑(AddEquiv.refl M) = AddMonoidHom.id M

source

ink

theorem MulEquiv.coe_monoidHom_refl {M : Type u_1} [inst : MulOneClass M] :

↑(MulEquiv.refl M) = MonoidHom.id M

source

ink

theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :

↑(AddEquiv.trans e₁ e₂) = AddMonoidHom.comp ↑e₂ ↑e₁

source

ink

theorem MulEquiv.coe_monoidHom_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) :

↑(MulEquiv.trans e₁ e₂) = MonoidHom.comp ↑e₂ ↑e₁

source

ink

theorem AddEquiv.ext {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {g : M ≃+ N} (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

Two additive isomorphisms agree if they are defined by the same underlying function.

source

ink

theorem MulEquiv.ext {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {g : M ≃* N} (h : ∀ (x : M), ↑f x = ↑g x) :

f = g

Two multiplicative isomorphisms agree if they are defined by the same underlying function.

source

ink

theorem AddEquiv.ext_iff {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {g : M ≃+ N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

source

ink

theorem MulEquiv.ext_iff {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {g : M ≃* N} :

f = g ↔ ∀ (x : M), ↑f x = ↑g x

source

ink

@[simp]

theorem AddEquiv.mk_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (e' : N → M) (h₁ : Function.LeftInverse e' ↑e) (h₂ : Function.RightInverse e' ↑e) (h₃ : ∀ (x y : M), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } y) :

{ toEquiv := { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = e

source

ink

@[simp]

theorem MulEquiv.mk_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (e' : N → M) (h₁ : Function.LeftInverse e' ↑e) (h₂ : Function.RightInverse e' ↑e) (h₃ : ∀ (x y : M), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } y) :

{ toEquiv := { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = e

source

ink

@[simp]

theorem AddEquiv.mk_coe' {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (f : N → M) (h₁ : Function.LeftInverse (↑e) f) (h₂ : Function.RightInverse (↑e) f) (h₃ : ∀ (x y : N), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) :

{ toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = AddEquiv.symm e

source

ink

@[simp]

theorem MulEquiv.mk_coe' {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (f : N → M) (h₁ : Function.LeftInverse (↑e) f) (h₂ : Function.RightInverse (↑e) f) (h₃ : ∀ (x y : N), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) :

{ toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = MulEquiv.symm e

source

ink

theorem AddEquiv.congr_arg {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {x : M} {x' : M} :

x = x' → ↑f x = ↑f x'

source

ink

theorem MulEquiv.congr_arg {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {x : M} {x' : M} :

x = x' → ↑f x = ↑f x'

source

ink

theorem AddEquiv.congr_fun {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {g : M ≃+ N} (h : f = g) (x : M) :

↑f x = ↑g x

source

ink

theorem MulEquiv.congr_fun {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {g : M ≃* N} (h : f = g) (x : M) :

↑f x = ↑g x

source

ink

def AddEquiv.addEquivOfUnique {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :

M ≃+ N

The AddEquiv between two AddMonoids with a unique element.

Equations

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

source

ink

def AddEquiv.addEquivOfUnique.proof_1 {M : Type u_2} {N : Type u_1} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :

∀ (x x_1 : M), Equiv.toFun { toFun := (Equiv.equivOfUnique M N).toFun, invFun := (Equiv.equivOfUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.equivOfUnique M N).toFun, invFun := (Equiv.equivOfUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun) } x + Equiv.toFun { toFun := (Equiv.equivOfUnique M N).toFun, invFun := (Equiv.equivOfUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun) } x_1

Equations

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

source

ink

def MulEquiv.mulEquivOfUnique {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Mul M] [inst : Mul N] :

M ≃* N

The MulEquiv between two monoids with a unique element.

Equations

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

source

ink

def AddEquiv.instUniqueAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :

∀ (x : M ≃+ N), x = default

Equations

(_ : x = default) = (_ : x = default)

source

ink

instance AddEquiv.instUniqueAddEquiv {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :

Unique (M ≃+ N)

There is a unique additive monoid homomorphism between two additive monoids with a unique element.

Equations

AddEquiv.instUniqueAddEquiv = { toInhabited := { default := AddEquiv.addEquivOfUnique }, uniq := (_ : ∀ (x : M ≃+ N), x = default) }

source

ink

instance MulEquiv.instUniqueMulEquiv {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Mul M] [inst : Mul N] :

Unique (M ≃* N)

There is a unique monoid homomorphism between two monoids with a unique element.

Equations

MulEquiv.instUniqueMulEquiv = { toInhabited := { default := MulEquiv.mulEquivOfUnique }, uniq := (_ : ∀ (x : M ≃* N), x = default) }

Monoids #

source

ink

theorem AddEquiv.map_zero {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) :

↑h 0 = 0

An additive isomorphism of additive monoids sends 0 to 0 (and is hence an additive monoid isomorphism).

source

ink

theorem MulEquiv.map_one {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) :

↑h 1 = 1

A multiplicative isomorphism of monoids sends 1 to 1 (and is hence a monoid isomorphism).

source

ink

theorem AddEquiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) {x : M} :

↑h x = 0 ↔ x = 0

source

ink

theorem MulEquiv.map_eq_one_iff {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) {x : M} :

↑h x = 1 ↔ x = 1

source

ink

theorem AddEquiv.map_ne_zero_iff {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) {x : M} :

↑h x ≠ 0 ↔ x ≠ 0

source

ink

theorem MulEquiv.map_ne_one_iff {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) {x : M} :

↑h x ≠ 1 ↔ x ≠ 1

source

ink

noncomputable def AddEquiv.ofBijective {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) (hf : Function.Bijective ↑f) :

M ≃+ N

A bijective AddSemigroup homomorphism is an isomorphism

Equations

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

source

ink

@[simp]

theorem AddEquiv.ofBijective_apply {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) (hf : Function.Bijective ↑f) (a : M) :

↑(AddEquiv.ofBijective f hf) a = ↑f a

source

ink

@[simp]

theorem MulEquiv.ofBijective_apply {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) (hf : Function.Bijective ↑f) (a : M) :

↑(MulEquiv.ofBijective f hf) a = ↑f a

source

ink

noncomputable def MulEquiv.ofBijective {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) (hf : Function.Bijective ↑f) :

M ≃* N

A bijective Semigroup homomorphism is an isomorphism

Equations

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

source

ink

@[simp]

theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective ↑f) :

↑f (↑(Equiv.symm (Equiv.ofBijective (↑f) hf)) n) = n

source

ink

@[simp]

theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective ↑f) :

↑f (↑(Equiv.symm (Equiv.ofBijective (↑f) hf)) n) = n

source

ink

def AddEquiv.toAddMonoidHom {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) :

M →+ N

Extract the forward direction of an additive equivalence as an addition-preserving function.

Equations

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

source

ink

def AddEquiv.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) (x : M) (y : M) :

Equiv.toFun h.toEquiv (x + y) = Equiv.toFun h.toEquiv x + Equiv.toFun h.toEquiv y

Equations

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

source

ink

def MulEquiv.toMonoidHom {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) :

M →* N

Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

Equations

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

source

ink

@[simp]

theorem AddEquiv.coe_toAddMonoidHom {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (e : M ≃+ N) :

↑(AddEquiv.toAddMonoidHom e) = ↑e

source

ink

@[simp]

theorem MulEquiv.coe_toMonoidHom {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (e : M ≃* N) :

↑(MulEquiv.toMonoidHom e) = ↑e

source

ink

theorem AddEquiv.toAddMonoidHom_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

Function.Injective AddEquiv.toAddMonoidHom

source

ink

theorem MulEquiv.toMonoidHom_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

Function.Injective MulEquiv.toMonoidHom

source

ink

def AddEquiv.arrowCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Add P] [inst : Add Q] (f : M ≃ N) (g : P ≃+ Q) :

(M → P) ≃+ (N → Q)

An additive analogue of Equiv.arrowCongr, where the equivalence between the targets is additive.

Equations

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

source

ink

def AddEquiv.arrowCongr.proof_1 {M : Type u_1} {N : Type u_4} {P : Type u_2} {Q : Type u_3} [inst : Add P] [inst : Add Q] (f : M ≃ N) (g : P ≃+ Q) (h : M → P) :

(fun k m => ↑(AddEquiv.symm g) (k (↑f m))) ((fun h n => ↑g (h (↑(Equiv.symm f) n))) h) = h

Equations

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

source

ink

def AddEquiv.arrowCongr.proof_3 {M : Type u_3} {N : Type u_1} {P : Type u_4} {Q : Type u_2} [inst : Add P] [inst : Add Q] (f : M ≃ N) (g : P ≃+ Q) (h : M → P) (k : M → P) :

Equiv.toFun { toFun := fun h n => ↑g (h (↑(Equiv.symm f) n)), invFun := fun k m => ↑(AddEquiv.symm g) (k (↑f m)), left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(AddEquiv.symm g) (k (↑f m))) ((fun h n => ↑g (h (↑(Equiv.symm f) n))) h) = h), right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (↑f m))) k) = k) } (h + k) = Equiv.toFun { toFun := fun h n => ↑g (h (↑(Equiv.symm f) n)), invFun := fun k m => ↑(AddEquiv.symm g) (k (↑f m)), left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(AddEquiv.symm g) (k (↑f m))) ((fun h n => ↑g (h (↑(Equiv.symm f) n))) h) = h), right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (↑f m))) k) = k) } h + Equiv.toFun { toFun := fun h n => ↑g (h (↑(Equiv.symm f) n)), invFun := fun k m => ↑(AddEquiv.symm g) (k (↑f m)), left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(AddEquiv.symm g) (k (↑f m))) ((fun h n => ↑g (h (↑(Equiv.symm f) n))) h) = h), right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (↑f m))) k) = k) } k

Equations

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

source

ink

def AddEquiv.arrowCongr.proof_2 {M : Type u_4} {N : Type u_1} {P : Type u_3} {Q : Type u_2} [inst : Add P] [inst : Add Q] (f : M ≃ N) (g : P ≃+ Q) (k : N → Q) :

(fun h n => ↑g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (↑f m))) k) = k

Equations

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

source

ink

@[simp]

theorem MulEquiv.arrowCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Mul P] [inst : Mul Q] (f : M ≃ N) (g : P ≃* Q) (h : M → P) (n : N) :

↑(MulEquiv.arrowCongr f g) h n = ↑g (h (↑(Equiv.symm f) n))

source

ink

@[simp]

theorem AddEquiv.arrowCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Add P] [inst : Add Q] (f : M ≃ N) (g : P ≃+ Q) (h : M → P) (n : N) :

↑(AddEquiv.arrowCongr f g) h n = ↑g (h (↑(Equiv.symm f) n))

source

ink

def MulEquiv.arrowCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Mul P] [inst : Mul Q] (f : M ≃ N) (g : P ≃* Q) :

(M → P) ≃* (N → Q)

A multiplicative analogue of Equiv.arrowCongr, where the equivalence between the targets is multiplicative.

Equations

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

source

ink

def AddEquiv.addMonoidHomCongr.proof_3 {M : Type u_1} {N : Type u_3} {P : Type u_2} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) (k : M →+ P) :

Equiv.toFun { toFun := fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := (_ : ∀ (h : M →+ P), (fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k) } (h + k) = Equiv.toFun { toFun := fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := (_ : ∀ (h : M →+ P), (fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k) } h + Equiv.toFun { toFun := fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := (_ : ∀ (h : M →+ P), (fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k) } k

Equations

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

source

ink

def AddEquiv.addMonoidHomCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) :

(M →+ P) ≃+ (N →+ Q)

An additive analogue of Equiv.arrowCongr, for additive maps from an additive monoid to a commutative additive monoid.

Equations

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

source

ink

def AddEquiv.addMonoidHomCongr.proof_2 {M : Type u_3} {N : Type u_1} {P : Type u_4} {Q : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (k : N →+ Q) :

(fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k

Equations

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

source

ink

def AddEquiv.addMonoidHomCongr.proof_1 {M : Type u_1} {N : Type u_3} {P : Type u_2} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :

(fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h

Equations

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

source

ink

@[simp]

theorem MulEquiv.monoidHomCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] [inst : CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :

↑(MulEquiv.monoidHomCongr f g) h = MonoidHom.comp (MulEquiv.toMonoidHom g) (MonoidHom.comp h (MulEquiv.toMonoidHom (MulEquiv.symm f)))

source

ink

@[simp]

theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :

↑(AddEquiv.addMonoidHomCongr f g) h = AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))

source

ink

def MulEquiv.monoidHomCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] [inst : CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) :

(M →* P) ≃* (N →* Q)

A multiplicative analogue of Equiv.arrowCongr, for multiplicative maps from a monoid to a commutative monoid.

Equations

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

source

ink

def AddEquiv.piCongrRight {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :

((j : η) → Ms j) ≃+ ((j : η) → Ns j)

A family of additive equivalences Π j, (Ms j ≃+ Ns j)≃+ Ns j) generates an additive equivalence between Π j, Ms j and Π j, Ns j.

This is the AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

Equations

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

source

ink

def AddEquiv.piCongrRight.proof_3 {η : Type u_1} {Ms : η → Type u_3} {Ns : η → Type u_2} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (y : (j : η) → Ms j) :

Equiv.toFun { toFun := fun x j => ↑(es j) (x j), invFun := fun x j => ↑(AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun) } (x + y) = Equiv.toFun { toFun := fun x j => ↑(es j) (x j), invFun := fun x j => ↑(AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun) } x + Equiv.toFun { toFun := fun x j => ↑(es j) (x j), invFun := fun x j => ↑(AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun) } y

Equations

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

source

ink

def AddEquiv.piCongrRight.proof_2 {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :

Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun

Equations

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

source

ink

def AddEquiv.piCongrRight.proof_1 {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :

Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun

Equations

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

source

ink

@[simp]

theorem AddEquiv.piCongrRight_apply {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :

↑(AddEquiv.piCongrRight es) x j = ↑(es j) (x j)

source

ink

@[simp]

theorem MulEquiv.piCongrRight_apply {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :

↑(MulEquiv.piCongrRight es) x j = ↑(es j) (x j)

source

ink

def MulEquiv.piCongrRight {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :

((j : η) → Ms j) ≃* ((j : η) → Ns j)

A family of multiplicative equivalences Π j, (Ms j ≃* Ns j)≃* Ns j) generates a multiplicative equivalence between Π j, Ms j and Π j, Ns j.

This is the MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

Equations

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

source

ink

@[simp]

theorem AddEquiv.piCongrRight_refl {η : Type u_1} {Ms : η → Type u_2} [inst : (j : η) → Add (Ms j)] :

(AddEquiv.piCongrRight fun j => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)

source

ink

@[simp]

theorem MulEquiv.piCongrRight_refl {η : Type u_1} {Ms : η → Type u_2} [inst : (j : η) → Mul (Ms j)] :

(MulEquiv.piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)

source

ink

@[simp]

theorem AddEquiv.piCongrRight_symm {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :

AddEquiv.symm (AddEquiv.piCongrRight es) = AddEquiv.piCongrRight fun i => AddEquiv.symm (es i)

source

ink

@[simp]

theorem MulEquiv.piCongrRight_symm {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :

MulEquiv.symm (MulEquiv.piCongrRight es) = MulEquiv.piCongrRight fun i => MulEquiv.symm (es i)

source

ink

@[simp]

theorem AddEquiv.piCongrRight_trans {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} {Ps : η → Type u_4} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] [inst : (j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :

AddEquiv.trans (AddEquiv.piCongrRight es) (AddEquiv.piCongrRight fs) = AddEquiv.piCongrRight fun i => AddEquiv.trans (es i) (fs i)

source

ink

@[simp]

theorem MulEquiv.piCongrRight_trans {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} {Ps : η → Type u_4} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] [inst : (j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :

MulEquiv.trans (MulEquiv.piCongrRight es) (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun i => MulEquiv.trans (es i) (fs i)

source

ink

def AddEquiv.piSubsingleton.proof_1 {ι : Type u_1} (M : ι → Type u_2) [inst : Subsingleton ι] (i : ι) :

Function.LeftInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun

Equations

(_ : Function.LeftInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun) = (_ : Function.LeftInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun)

source

ink

def AddEquiv.piSubsingleton.proof_3 {ι : Type u_2} (M : ι → Type u_1) [inst : (j : ι) → Add (M j)] (i : ι) :

∀ (x x_1 : (j : ι) → M j), (((i : ι) → M i) + ((i : ι) → M i)) ((i : ι) → M i) instHAdd x x_1 i = x i + x_1 i

Equations

(_ : (((i : ι) → M i) + ((i : ι) → M i)) ((i : ι) → M i) instHAdd x x i = x i + x i) = (_ : (((i : ι) → M i) + ((i : ι) → M i)) ((i : ι) → M i) instHAdd x x i = x i + x i)

source

ink

def AddEquiv.piSubsingleton.proof_2 {ι : Type u_1} (M : ι → Type u_2) [inst : Subsingleton ι] (i : ι) :

Function.RightInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun

Equations

(_ : Function.RightInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun) = (_ : Function.RightInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun)

source

ink

def AddEquiv.piSubsingleton {ι : Type u_1} (M : ι → Type u_2) [inst : (j : ι) → Add (M j)] [inst : Subsingleton ι] (i : ι) :

((j : ι) → M j) ≃+ M i

A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

Equations

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

source

ink

@[simp]

theorem MulEquiv.piSubsingleton_apply {ι : Type u_1} (M : ι → Type u_2) [inst : (j : ι) → Mul (M j)] [inst : Subsingleton ι] (i : ι) (f : (x : ι) → M x) :

↑(MulEquiv.piSubsingleton M i) f = f i

source

ink

@[simp]

theorem AddEquiv.piSubsingleton_symm_apply {ι : Type u_1} (M : ι → Type u_2) [inst : (j : ι) → Add (M j)] [inst : Subsingleton ι] (i : ι) (x : M i) (b : ι) :

↑(AddEquiv.symm (AddEquiv.piSubsingleton M i)) x b = cast (_ : M i = M b) x

source

ink

@[simp]

theorem MulEquiv.piSubsingleton_symm_apply {ι : Type u_1} (M : ι → Type u_2) [inst : (j : ι) → Mul (M j)] [inst : Subsingleton ι] (i : ι) (x : M i) (b : ι) :

↑(MulEquiv.symm (MulEquiv.piSubsingleton M i)) x b = cast (_ : M i = M b) x

source

ink

@[simp]

theorem AddEquiv.piSubsingleton_apply {ι : Type u_1} (M : ι → Type u_2) [inst : (j : ι) → Add (M j)] [inst : Subsingleton ι] (i : ι) (f : (x : ι) → M x) :

↑(AddEquiv.piSubsingleton M i) f = f i

source

ink

def MulEquiv.piSubsingleton {ι : Type u_1} (M : ι → Type u_2) [inst : (j : ι) → Mul (M j)] [inst : Subsingleton ι] (i : ι) :

((j : ι) → M j) ≃* M i

A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

Equations

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

Groups #

source

ink

theorem AddEquiv.map_neg {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : SubtractionMonoid H] (h : G ≃+ H) (x : G) :

↑h (-x) = -↑h x

An additive equivalence of additive groups preserves negation.

source

ink

theorem MulEquiv.map_inv {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : DivisionMonoid H] (h : G ≃* H) (x : G) :

↑h x⁻¹ = (↑h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

source

ink

theorem AddEquiv.map_sub {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : SubtractionMonoid H] (h : G ≃+ H) (x : G) (y : G) :

↑h (x - y) = ↑h x - ↑h y

An additive equivalence of additive groups preserves subtractions.

source

ink

theorem MulEquiv.map_div {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : DivisionMonoid H] (h : G ≃* H) (x : G) (y : G) :

↑h (x / y) = ↑h x / ↑h y

A multiplicative equivalence of groups preserves division.

source

ink

def AddHom.toAddEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) :

M ≃+ N

Given a pair of additive homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive homomorphisms.

Equations

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

source

ink

def AddHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₂ : AddHom.comp f g = AddHom.id N) (x : N) :

↑(AddHom.comp f g) x = ↑(AddHom.id N) x

Equations

(_ : ∀ (x : N), ↑(AddHom.comp f g) x = ↑(AddHom.id N) x) = (_ : ∀ (x : N), ↑(AddHom.comp f g) x = ↑(AddHom.id N) x)

source

ink

def AddHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (x : M) :

↑(AddHom.comp g f) x = ↑(AddHom.id M) x

Equations

(_ : ∀ (x : M), ↑(AddHom.comp g f) x = ↑(AddHom.id M) x) = (_ : ∀ (x : M), ↑(AddHom.comp g f) x = ↑(AddHom.id M) x)

source

ink

def MulHom.toMulEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) :

M ≃* N

Given a pair of multiplicative homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an multiplicative equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for multiplicative homomorphisms.

Equations

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

source

ink

@[simp]

theorem AddHom.toAddEquiv_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) :

↑(AddHom.toAddEquiv f g h₁ h₂) = ↑f

source

ink

@[simp]

theorem MulHom.toMulEquiv_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) :

↑(MulHom.toMulEquiv f g h₁ h₂) = ↑f

source

ink

@[simp]

theorem AddHom.toAddEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) :

↑(AddEquiv.symm (AddHom.toAddEquiv f g h₁ h₂)) = ↑g

source

ink

@[simp]

theorem MulHom.toMulEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) :

↑(MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂)) = ↑g

source

ink

def AddMonoidHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (x : M) :

↑(AddMonoidHom.comp g f) x = ↑(AddMonoidHom.id M) x

Equations

(_ : ∀ (x : M), ↑(AddMonoidHom.comp g f) x = ↑(AddMonoidHom.id M) x) = (_ : ∀ (x : M), ↑(AddMonoidHom.comp g f) x = ↑(AddMonoidHom.id M) x)

source

ink

def AddMonoidHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) (x : N) :

↑(AddMonoidHom.comp f g) x = ↑(AddMonoidHom.id N) x

Equations

(_ : ∀ (x : N), ↑(AddMonoidHom.comp f g) x = ↑(AddMonoidHom.id N) x) = (_ : ∀ (x : N), ↑(AddMonoidHom.comp f g) x = ↑(AddMonoidHom.id N) x)

source

ink

def AddMonoidHom.toAddEquiv {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) :

M ≃+ N

Given a pair of additive monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

Equations

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

source

ink

@[simp]

theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) :

↑(MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂)) = ↑g

source

ink

@[simp]

theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) :

↑(AddEquiv.symm (AddMonoidHom.toAddEquiv f g h₁ h₂)) = ↑g

source

ink

@[simp]

theorem AddMonoidHom.toAddEquiv_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) :

↑(AddMonoidHom.toAddEquiv f g h₁ h₂) = ↑f

source

ink

@[simp]

theorem MonoidHom.toMulEquiv_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) :

↑(MonoidHom.toMulEquiv f g h₁ h₂) = ↑f

source

ink

def MonoidHom.toMulEquiv {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) :

M ≃* N

Given a pair of monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an multiplicative equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for monoid homomorphisms.

Equations