isOrtho_smul_right — Mathlib

English

If a ≠ 0, then scaling the second argument preserves orthogonality: IsOrtho G x (a · y) ↔ IsOrtho G x y.

Русский

Если a ≠ 0, масштабирование второго аргумента сохраняет ортогональность: IsOrtho G x (a · y) ↔ IsOrtho G x y.

LaTeX

$$$ a \\neq 0 \\Rightarrow (G.IsOrtho x (a \\cdot y) \\iff G.IsOrtho x y) $$$

Lean4

@[simp]
theorem isOrtho_smul_right {x y : M₄} {a : R₄} (ha : a ≠ 0) : IsOrtho G x (a • y) ↔ IsOrtho G x y :=
  by
  dsimp only [IsOrtho]
  rw [map_smul]
  simp only [smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]
  exact fun a ↦ (ha a).elim

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