smul_units_def — Mathlib

English

The smul action of an automorphism on a unit equals the Units.map of that automorphism applied to the unit.

Русский

Действие скаляра автоморфизма на единицу равняется отображению единицы через соответствующий автоморфизм единиц.

LaTeX

$$$ f \\cdot x = \\mathrm{Units.map}(f)\\,x, \\; f:\\mathrm{AlgEquiv}_R(A_1,A_1),\\; x\\in A_1^\\times.$$$

Lean4

@[simp]
theorem smul_units_def (f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) : f • x = Units.map f x :=
  rfl

Похожие утверждения