Documentation

Mathlib.Algebra.Ring.AddAut

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
    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
        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⁻¹