smul_mem_of_mem — Mathlib

English

If r is unitary in R and a is unitary in A, then their combined action r • a is unitary in A.

Русский

Если r унитарен в R, а a унитарен в A, то действие r • a остается унитарным в A.

LaTeX

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

Lean4

theorem smul_mem_of_mem {r : R} {a : A} (hr : r ∈ unitary R) (ha : a ∈ unitary A) : r • a ∈ unitary A := by
  simp [mem_iff, smul_smul, mul_smul_comm, smul_mul_assoc, hr, ha]

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