# 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.

source
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

Instances For

source
@[simp]
theorem AddAut.mulLeft_apply_symm_apply {R : Type u_1} [Semiring R] (x : R ˣ) (a✝ : R) :
(AddEquiv.symm (mulLeft x)) a✝ = x⁻¹ • a✝
source
@[simp]
theorem AddAut.mulLeft_apply_apply {R : Type u_1} [Semiring R] (x : R ˣ) (a✝ : R) :
(mulLeft x) a✝ = x • a✝
source
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) (Units.opEquiv.symm (MulOpposite.op u))

Instances For

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