ortho_smul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ortho_smul_right {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V} {x y} {a : K₂} {ha : a ≠ 0} :
    IsOrtho B x y ↔ IsOrtho B x (a • 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
    · simp only [map_eq_zero] at H
      exfalso
      exact ha H
    · exact H

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