mathlib3 documentation

algebra.ring.add_aut

Multiplication on the left/right as additive automorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define add_aut.mul_left and add_aut.mul_right.

See also add_monoid_hom.mul_left, add_monoid_hom.mul_right, add_monoid.End.mul_left, and add_monoid.End.mul_right for multiplication by R as an endomorphism instead of multiplication by as an automorphism.

def add_aut.mul_left {R : Type u_1} [semiring R] :

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

Equations
@[simp]
theorem add_aut.mul_left_apply_symm_apply {R : Type u_1} [semiring R] (x : Rˣ) (ᾰ : R) :
@[simp]
theorem add_aut.mul_left_apply_apply {R : Type u_1} [semiring R] (x : Rˣ) (ᾰ : R) :
def add_aut.mul_right {R : Type u_1} [semiring R] (u : Rˣ) :

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

Equations
@[simp]
theorem add_aut.mul_right_apply {R : Type u_1} [semiring R] (u : Rˣ) (x : R) :
@[simp]
theorem add_aut.mul_right_symm_apply {R : Type u_1} [semiring R] (u : Rˣ) (x : R) :