smul_mem — Mathlib

English

The natural action of unitary elements of R on unitary elements of A is well-defined, yielding a unitary element of A.

Русский

Натуральное действие унитарных элементов R на унитарных элементах A определено и даёт унитарный элемент A.

LaTeX

$$$r \\in \\mathrm{unitary}(R),\\ a \\in \\mathrm{unitary}(A) \\Rightarrow r \\cdot a \\in \\mathrm{unitary}(A)$$$

Lean4

theorem smul_mem (r : unitary R) {a : A} (ha : a ∈ unitary A) : r • a ∈ unitary A :=
  smul_mem_of_mem (R := R) r.prop ha

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