Multiplicative and additive equivalence acting on units.

ink

def toAddUnits.proof_1 {G : Type u_1} [inst : AddGroup G] : ∀ (x : G), (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)

Equations

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

ink

def toAddUnits.proof_3 {G : Type u_1} [inst : AddGroup G] : ∀ (x x_1 : G), Equiv.toFun { toFun := fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }, invFun := fun x => ↑x, left_inv := (_ : ∀ (x : G), (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)), right_inv := (_ : ∀ (x : AddUnits G), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => ↑x) x) = x) } (x + x_1) = Equiv.toFun { toFun := fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }, invFun := fun x => ↑x, left_inv := (_ : ∀ (x : G), (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)), right_inv := (_ : ∀ (x : AddUnits G), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => ↑x) x) = x) } x + Equiv.toFun { toFun := fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }, invFun := fun x => ↑x, left_inv := (_ : ∀ (x : G), (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => ↑x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)), right_inv := (_ : ∀ (x : AddUnits G), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => ↑x) x) = x) } x_1

Equations

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

ink

def toAddUnits.proof_2 {G : Type u_1} [inst : AddGroup G] : ∀ (x : AddUnits G), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => ↑x) x) = x

Equations

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

ink

def toAddUnits {G : Type u_1} [inst : AddGroup G] : G ≃+ AddUnits G

An additive group is isomorphic to its group of additive units

Equations

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

ink

def toUnits {G : Type u_1} [inst : Group G] : G ≃* Gˣ

A group is isomorphic to its group of units.

Equations

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

ink

@[simp]

theorem coe_toAddUnits {G : Type u_1} [inst : AddGroup G] (g : G) : ↑(↑toAddUnits g) = g

ink

@[simp]

theorem coe_toUnits {G : Type u_1} [inst : Group G] (g : G) : ↑(↑toUnits g) = g

ink

def Units.mapEquiv {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (h : M ≃* N) : Mˣ ≃* Nˣ

A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

Equations

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

ink

@[simp]

theorem Units.mapEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (h : M ≃* N) : MulEquiv.symm (Units.mapEquiv h) = Units.mapEquiv (MulEquiv.symm h)

ink

@[simp]

theorem Units.coe_mapEquiv {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (h : M ≃* N) (x : Mˣ) : ↑(↑(Units.mapEquiv h) x) = ↑h ↑x

ink

def AddUnits.addLeft {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : Equiv.Perm M

Left addition of an additive unit is a permutation of the underlying type.

Equations

• AddUnits.addLeft u = { toFun := fun x => ↑u + x, invFun := fun x => ↑(-u) + x, left_inv := (_ : ∀ (b : M), ↑(-u) + (↑u + b) = b), right_inv := (_ : ∀ (b : M), ↑u + (↑(-u) + b) = b) }

ink

@[simp]

theorem AddUnits.addLeft_apply {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : ↑(AddUnits.addLeft u) = fun x => ↑u + x

ink

@[simp]

theorem Units.mulLeft_apply {M : Type u_1} [inst : Monoid M] (u : Mˣ) : ↑(Units.mulLeft u) = fun x => ↑u * x

ink

def Units.mulLeft {M : Type u_1} [inst : Monoid M] (u : Mˣ) : Equiv.Perm M

Left multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

• Units.mulLeft u = { toFun := fun x => ↑u * x, invFun := fun x => ↑u⁻¹ * x, left_inv := (_ : ∀ (b : M), ↑u⁻¹ * (↑u * b) = b), right_inv := (_ : ∀ (b : M), ↑u * (↑u⁻¹ * b) = b) }

ink

@[simp]

theorem AddUnits.addLeft_symm {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : Equiv.symm (AddUnits.addLeft u) = AddUnits.addLeft (-u)

ink

@[simp]

theorem Units.mulLeft_symm {M : Type u_1} [inst : Monoid M] (u : Mˣ) : Equiv.symm (Units.mulLeft u) = Units.mulLeft u⁻¹

ink

theorem AddUnits.addLeft_bijective {M : Type u_1} [inst : AddMonoid M] (a : AddUnits M) : Function.Bijective fun x => ↑a + x

ink

theorem Units.mulLeft_bijective {M : Type u_1} [inst : Monoid M] (a : Mˣ) : Function.Bijective fun x => ↑a * x

ink

def AddUnits.addRight.proof_2 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M) : x + ↑(-u) + ↑u = x

Equations

• (_ : x + ↑(-u) + ↑u = x) = (_ : x + ↑(-u) + ↑u = x)

ink

def AddUnits.addRight {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : Equiv.Perm M

Right addition of an additive unit is a permutation of the underlying type.

Equations

• AddUnits.addRight u = { toFun := fun x => x + ↑u, invFun := fun x => x + ↑(-u), left_inv := (_ : ∀ (x : M), x + ↑u + ↑(-u) = x), right_inv := (_ : ∀ (x : M), x + ↑(-u) + ↑u = x) }

ink

def AddUnits.addRight.proof_1 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M) : x + ↑u + ↑(-u) = x

Equations

• (_ : x + ↑u + ↑(-u) = x) = (_ : x + ↑u + ↑(-u) = x)

ink

@[simp]

theorem AddUnits.addRight_apply {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : ↑(AddUnits.addRight u) = fun x => x + ↑u

ink

@[simp]

theorem Units.mulRight_apply {M : Type u_1} [inst : Monoid M] (u : Mˣ) : ↑(Units.mulRight u) = fun x => x * ↑u

ink

def Units.mulRight {M : Type u_1} [inst : Monoid M] (u : Mˣ) : Equiv.Perm M

Right multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

• Units.mulRight u = { toFun := fun x => x * ↑u, invFun := fun x => x * ↑u⁻¹, left_inv := (_ : ∀ (x : M), x * ↑u * ↑u⁻¹ = x), right_inv := (_ : ∀ (x : M), x * ↑u⁻¹ * ↑u = x) }

ink

@[simp]

theorem AddUnits.addRight_symm {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : Equiv.symm (AddUnits.addRight u) = AddUnits.addRight (-u)

ink

@[simp]

theorem Units.mulRight_symm {M : Type u_1} [inst : Monoid M] (u : Mˣ) : Equiv.symm (Units.mulRight u) = Units.mulRight u⁻¹

ink

theorem AddUnits.addRight_bijective {M : Type u_1} [inst : AddMonoid M] (a : AddUnits M) : Function.Bijective fun x => x + ↑a

ink

theorem Units.mulRight_bijective {M : Type u_1} [inst : Monoid M] (a : Mˣ) : Function.Bijective fun x => x * ↑a

ink

def Equiv.addLeft {G : Type u_1} [inst : AddGroup G] (a : G) : Equiv.Perm G

Left addition in an AddGroup is a permutation of the underlying type.

Equations

• Equiv.addLeft a = AddUnits.addLeft (↑toAddUnits a)

ink

def Equiv.mulLeft {G : Type u_1} [inst : Group G] (a : G) : Equiv.Perm G

Left multiplication in a Group is a permutation of the underlying type.

Equations

• Equiv.mulLeft a = Units.mulLeft (↑toUnits a)

ink

@[simp]

theorem Equiv.coe_addLeft {G : Type u_1} [inst : AddGroup G] (a : G) : ↑(Equiv.addLeft a) = (fun x x_1 => x + x_1) a

ink

@[simp]

theorem Equiv.coe_mulLeft {G : Type u_1} [inst : Group G] (a : G) : ↑(Equiv.mulLeft a) = (fun x x_1 => x * x_1) a

ink

theorem Equiv.addLeft_symm_apply {G : Type u_1} [inst : AddGroup G] (a : G) : ↑(Equiv.symm (Equiv.addLeft a)) = fun x => -a + x

Extra simp lemma that dsimp can use. simp will never use this.

ink

@[simp]

theorem Equiv.mulLeft_symm_apply {G : Type u_1} [inst : Group G] (a : G) : ↑(Equiv.symm (Equiv.mulLeft a)) = fun x => a⁻¹ * x

Extra simp lemma that dsimp can use. simp will never use this.

ink

@[simp]

theorem Equiv.addLeft_symm {G : Type u_1} [inst : AddGroup G] (a : G) : Equiv.symm (Equiv.addLeft a) = Equiv.addLeft (-a)

ink

@[simp]

theorem Equiv.mulLeft_symm {G : Type u_1} [inst : Group G] (a : G) : Equiv.symm (Equiv.mulLeft a) = Equiv.mulLeft a⁻¹

ink

theorem AddGroup.addLeft_bijective {G : Type u_1} [inst : AddGroup G] (a : G) : Function.Bijective fun x => a + x

ink

theorem Group.mulLeft_bijective {G : Type u_1} [inst : Group G] (a : G) : Function.Bijective fun x => a * x

ink

def Equiv.addRight {G : Type u_1} [inst : AddGroup G] (a : G) : Equiv.Perm G

Right addition in an AddGroup is a permutation of the underlying type.

Equations

• Equiv.addRight a = AddUnits.addRight (↑toAddUnits a)

ink

def Equiv.mulRight {G : Type u_1} [inst : Group G] (a : G) : Equiv.Perm G

Right multiplication in a Group is a permutation of the underlying type.

Equations

• Equiv.mulRight a = Units.mulRight (↑toUnits a)

ink

@[simp]

theorem Equiv.coe_addRight {G : Type u_1} [inst : AddGroup G] (a : G) : ↑(Equiv.addRight a) = fun x => x + a

ink

@[simp]

theorem Equiv.coe_mulRight {G : Type u_1} [inst : Group G] (a : G) : ↑(Equiv.mulRight a) = fun x => x * a

ink

@[simp]

theorem Equiv.addRight_symm {G : Type u_1} [inst : AddGroup G] (a : G) : Equiv.symm (Equiv.addRight a) = Equiv.addRight (-a)

ink

@[simp]

theorem Equiv.mulRight_symm {G : Type u_1} [inst : Group G] (a : G) : Equiv.symm (Equiv.mulRight a) = Equiv.mulRight a⁻¹

ink

theorem Equiv.addRight_symm_apply {G : Type u_1} [inst : AddGroup G] (a : G) : ↑(Equiv.symm (Equiv.addRight a)) = fun x => x + -a

Extra simp lemma that dsimp can use. simp will never use this.

ink

@[simp]

theorem Equiv.mulRight_symm_apply {G : Type u_1} [inst : Group G] (a : G) : ↑(Equiv.symm (Equiv.mulRight a)) = fun x => x * a⁻¹

Extra simp lemma that dsimp can use. simp will never use this.

ink

theorem AddGroup.addRight_bijective {G : Type u_1} [inst : AddGroup G] (a : G) : Function.Bijective fun x => x + a

ink

theorem Group.mulRight_bijective {G : Type u_1} [inst : Group G] (a : G) : Function.Bijective fun x => x * a

ink

def Equiv.subLeft.proof_2 {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : a - (-b + a) = b

Equations

• (_ : a - (-b + a) = b) = (_ : a - (-b + a) = b)

ink

def Equiv.subLeft.proof_1 {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : -(a - b) + a = b

Equations

• (_ : -(a - b) + a = b) = (_ : -(a - b) + a = b)

ink

def Equiv.subLeft {G : Type u_1} [inst : AddGroup G] (a : G) : G ≃ G

A version of Equiv.addLeft a (-b) that is defeq to a - b.

Equations

• Equiv.subLeft a = { toFun := fun b => a - b, invFun := fun b => -b + a, left_inv := (_ : ∀ (b : G), -(a - b) + a = b), right_inv := (_ : ∀ (b : G), a - (-b + a) = b) }

ink

@[simp]

theorem Equiv.divLeft_symm_apply {G : Type u_1} [inst : Group G] (a : G) (b : G) : ↑(Equiv.symm (Equiv.divLeft a)) b = b⁻¹ * a

ink

@[simp]

theorem Equiv.divLeft_apply {G : Type u_1} [inst : Group G] (a : G) (b : G) : ↑(Equiv.divLeft a) b = a / b

ink

@[simp]

theorem Equiv.subLeft_symm_apply {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : ↑(Equiv.symm (Equiv.subLeft a)) b = -b + a

ink

@[simp]

theorem Equiv.subLeft_apply {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : ↑(Equiv.subLeft a) b = a - b

ink

def Equiv.divLeft {G : Type u_1} [inst : Group G] (a : G) : G ≃ G

A version of Equiv.mulLeft a b⁻¹⁻¹ that is defeq to a / b.

Equations

• Equiv.divLeft a = { toFun := fun b => a / b, invFun := fun b => b⁻¹ * a, left_inv := (_ : ∀ (b : G), (a / b)⁻¹ * a = b), right_inv := (_ : ∀ (b : G), a / (b⁻¹ * a) = b) }

ink

theorem Equiv.subLeft_eq_neg_trans_addLeft {G : Type u_1} [inst : AddGroup G] (a : G) : Equiv.subLeft a = Equiv.trans (Equiv.neg G) (Equiv.addLeft a)

ink

theorem Equiv.divLeft_eq_inv_trans_mulLeft {G : Type u_1} [inst : Group G] (a : G) : Equiv.divLeft a = Equiv.trans (Equiv.inv G) (Equiv.mulLeft a)

ink

def Equiv.subRight {G : Type u_1} [inst : AddGroup G] (a : G) : G ≃ G

A version of Equiv.addRight (-a) b that is defeq to b - a.

Equations

• Equiv.subRight a = { toFun := fun b => b - a, invFun := fun b => b + a, left_inv := (_ : ∀ (b : G), b - a + a = b), right_inv := (_ : ∀ (b : G), b + a - a = b) }

ink

def Equiv.subRight.proof_2 {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : b + a - a = b

Equations

• (_ : b + a - a = b) = (_ : b + a - a = b)

ink

def Equiv.subRight.proof_1 {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : b - a + a = b

Equations

• (_ : b - a + a = b) = (_ : b - a + a = b)

ink

@[simp]

theorem Equiv.subRight_symm_apply {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : ↑(Equiv.symm (Equiv.subRight a)) b = b + a

ink

@[simp]

theorem Equiv.divRight_apply {G : Type u_1} [inst : Group G] (a : G) (b : G) : ↑(Equiv.divRight a) b = b / a

ink

@[simp]

theorem Equiv.divRight_symm_apply {G : Type u_1} [inst : Group G] (a : G) (b : G) : ↑(Equiv.symm (Equiv.divRight a)) b = b * a

ink

@[simp]

theorem Equiv.subRight_apply {G : Type u_1} [inst : AddGroup G] (a : G) (b : G) : ↑(Equiv.subRight a) b = b - a

ink

def Equiv.divRight {G : Type u_1} [inst : Group G] (a : G) : G ≃ G

A version of Equiv.mulRight a⁻¹ b⁻¹ b that is defeq to b / a.

Equations

• Equiv.divRight a = { toFun := fun b => b / a, invFun := fun b => b * a, left_inv := (_ : ∀ (b : G), b / a * a = b), right_inv := (_ : ∀ (b : G), b * a / a = b) }

ink

theorem Equiv.subRight_eq_addRight_neg {G : Type u_1} [inst : AddGroup G] (a : G) : Equiv.subRight a = Equiv.addRight (-a)

ink

theorem Equiv.divRight_eq_mulRight_inv {G : Type u_1} [inst : Group G] (a : G) : Equiv.divRight a = Equiv.mulRight a⁻¹

ink

def AddEquiv.neg (G : Type u_1) [inst : SubtractionCommMonoid G] : G ≃+ G

When the AddGroup is commutative, Equiv.neg is an AddEquiv.

Equations

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

ink

@[simp]

theorem AddEquiv.neg_apply (G : Type u_1) [inst : SubtractionCommMonoid G] : ∀ (a : G), ↑(AddEquiv.neg G) a = -a

ink

@[simp]

theorem MulEquiv.inv_apply (G : Type u_1) [inst : DivisionCommMonoid G] : ∀ (a : G), ↑(MulEquiv.inv G) a = a⁻¹

ink

def MulEquiv.inv (G : Type u_1) [inst : DivisionCommMonoid G] : G ≃* G

In a DivisionCommMonoid, Equiv.inv is a MulEquiv. There is a variant of this MulEquiv.inv' G : G ≃* Gᵐᵒᵖ≃* Gᵐᵒᵖ for the non-commutative case.

Equations

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

ink

@[simp]

theorem AddEquiv.neg_symm (G : Type u_1) [inst : SubtractionCommMonoid G] : AddEquiv.symm (AddEquiv.neg G) = AddEquiv.neg G

ink

@[simp]

theorem MulEquiv.inv_symm (G : Type u_1) [inst : DivisionCommMonoid G] : MulEquiv.symm (MulEquiv.inv G) = MulEquiv.inv G