Multiplication on the left/right as additive automorphisms

In this file we define AddAut.mulLeft and AddAut.mulRight.

See also AddMonoidHom.mulLeft, AddMonoidHom.mulRight, AddMonoid.End.mulLeft, and AddMonoid.End.mulRight for multiplication by R as an endomorphism instead of multiplication by Rˣ as an automorphism.

@[simp]

theorem AddAut.mulLeft_apply_symm_apply {R : Type u_1} [Semiring R] (x : Rˣ) : ∀ (a : R), ↑(AddEquiv.symm (↑AddAut.mulLeft x)) a = x⁻¹ • a

@[simp]

theorem AddAut.mulLeft_apply_apply {R : Type u_1} [Semiring R] (x : Rˣ) : ∀ (a : R), ↑(↑AddAut.mulLeft x) a = x • a

def AddAut.mulLeft {R : Type u_1} [Semiring R] : Rˣ →* AddAut R

Left multiplication by a unit of a semiring as an additive automorphism.

Equations

• AddAut.mulLeft = DistribMulAction.toAddAut Rˣ R

def AddAut.mulRight {R : Type u_1} [Semiring R] (u : Rˣ) : AddAut R

Right multiplication by a unit of a semiring as an additive automorphism.

Equations

• AddAut.mulRight u = ↑(DistribMulAction.toAddAut Rᵐᵒᵖˣ R) (↑(MulEquiv.symm Units.opEquiv) (MulOpposite.op u))

@[simp]

theorem AddAut.mulRight_apply {R : Type u_1} [Semiring R] (u : Rˣ) (x : R) : ↑(AddAut.mulRight u) x = x * ↑u

@[simp]

theorem AddAut.mulRight_symm_apply {R : Type u_1} [Semiring R] (u : Rˣ) (x : R) : ↑(AddEquiv.symm (AddAut.mulRight u)) x = x * ↑u⁻¹