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
Rˣ as an automorphism.
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) :
⇑(add_equiv.symm (⇑add_aut.mul_left x)) ᾰ = x⁻¹ • ᾰ
@[simp]
theorem
add_aut.mul_left_apply_apply
{R : Type u_1}
[semiring R]
(x : Rˣ)
(ᾰ : R) :
⇑(⇑add_aut.mul_left x) ᾰ = x • ᾰ
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) :
⇑(add_aut.mul_right u) x = x * ↑u
@[simp]
theorem
add_aut.mul_right_symm_apply
{R : Type u_1}
[semiring R]
(u : Rˣ)
(x : R) :
⇑(add_equiv.symm (add_aut.mul_right u)) x = x * ↑u⁻¹