isOrtho_smul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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