# 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} [] (x : Rˣ) :
@[simp]
theorem AddAut.mulLeft_apply_apply {R : Type u_1} [] (x : Rˣ) :
∀ (a : R), (AddAut.mulLeft x) a = x a
def AddAut.mulLeft {R : Type u_1} [] :

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

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

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

Equations
• = (Units.opEquiv.symm ())
Instances For
@[simp]
theorem AddAut.mulRight_apply {R : Type u_1} [] (u : Rˣ) (x : R) :
() x = x * u
@[simp]
theorem AddAut.mulRight_symm_apply {R : Type u_1} [] (u : Rˣ) (x : R) :
() x = x * u⁻¹