instSMulRat — Mathlib

English

There is a scalar action of the rationals Q on the self-adjoint elements of R, i.e., for any q ∈ Q and x ∈ selfAdjoint(R), q • x ∈ selfAdjoint(R).

Русский

Существует скалярное действие рациональных чисел Q на самосопряжённых элементах R: для любого q ∈ Q и x ∈ selfAdjoint(R) результат q • x принадлежит selfAdjoint(R).

LaTeX

$$$ \\forall q \\in \\mathbb{Q}, \\; \\forall x \\in \\mathrm{selfAdjoint}(R), \\; q \\cdot x \\in \\mathrm{selfAdjoint}(R). $$$

Lean4

instance instSMulRat : SMul ℚ (selfAdjoint R) where
  smul a x := ⟨a • (x : R), by rw [Rat.smul_def]; exact .mul (.ratCast a) x.prop⟩

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