ortho_smul_left — Mathlib

English

If a ≠ 0, then IsOrtho(B, x, y) is equivalent to IsOrtho(B, a·x, y).

Русский

Если a ≠ 0, то IsOrtho(B, x, y) эквивалентно IsOrtho(B, a·x, y).

LaTeX

$$$a \\ne 0 \\Rightarrow (B.IsOrtho(x,y) \\iff B.IsOrtho(a\\cdot x, y))$$$

Lean4

theorem ortho_smul_left {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V} {x y} {a : K₁} (ha : a ≠ 0) :
    IsOrtho B x y ↔ IsOrtho B (a • x) y := by
  dsimp only [IsOrtho]
  constructor <;> intro H
  · rw [map_smulₛₗ₂, H, smul_zero]
  · rw [map_smulₛₗ₂, smul_eq_zero] at H
    rcases H with H | H
    · rw [map_eq_zero I₁] at H
      trivial
    · exact H

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