smul_right — Mathlib

English

If v ⟂ᵥ w then v ⟂ᵥ r • w for any scalar r (with appropriate structure).

Русский

Если v ⟂ᵥ w, то v ⟂ᵥ r • w для любого скаляра r (при наличии нужного алгебраического структура).

LaTeX

$$$ v \\perp_{\\mathcal{V}} w \\Rightarrow v \\perp_{\\mathcal{V}} (r \\cdot w) $$$

Lean4

theorem smul_right {R : Type*} [Semiring R] [DistribMulAction R N] [ContinuousConstSMul R N] (r : R) (h : v ⟂ᵥ w) :
    v ⟂ᵥ r • w :=
  let ⟨s, hmeas, hs₁, hs₂⟩ := h
  ⟨s, hmeas, hs₁, fun t ht => by simp only [coe_smul, Pi.smul_apply, hs₂ t ht, smul_zero]⟩

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