unitsMulSemiringAction — Mathlib

English

Let ConjAct be the action by units of a ring. The units of R act on R by left multiplication; this action is a MulSemiringAction, preserving zero and addition in R.

Русский

Пусть ConjAct — это действие единиц кольца. Единицы R действуют на R посредством умножения слева; это действие удовлетворяет условиям MulSemiringAction и сохраняет ноль и сложение.

LaTeX

$$$\\forall u:\\, \\mathrm{Units}(R),\\; x:\\, R:\\; u \\cdot x = u x$$$

Lean4

instance unitsMulSemiringAction : MulSemiringAction (ConjAct Rˣ) R :=
  { ConjAct.unitsMulDistribMulAction with
    smul_zero := by simp [units_smul_def]
    smul_add := by simp [units_smul_def, mul_add, add_mul] }

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