isOrthogonal_of_forall_apply_same

English

If 2 is left-regular in R, B is symmetric, and B(fx, fx) = B(x, x) for all x, then f is orthogonal with respect to B.

Русский

Если 2 есть левый делитель нуля в R, B симметрична, и B(fx, fx) = B(x, x) для всех x, то f ортогонален относительно B.

LaTeX

$$(IsLeftRegular(2) ∧ B.IsSymm ∧ ∀x, B(fx, fx) = B(x, x)) → ∀x,y, B(fx, fy) = B(x, y)$$

Lean4

theorem isOrthogonal_of_forall_apply_same {F : Type*} [FunLike F M M] [LinearMapClass F R M M] (f : F)
    (h : IsLeftRegular (2 : R)) (hB : B.IsSymm) (hf : ∀ x, B (f x) (f x) = B x x) : B.IsOrthogonal f :=
  by
  intro x y
  suffices 2 * B (f x) (f y) = 2 * B x y from h this
  have := hf (x + y)
  simp only [map_add, LinearMap.add_apply, hf x, hf y, show B y x = B x y from hB.eq y x] at this
  rw [show B (f y) (f x) = B (f x) (f y) from hB.eq (f y) (f x)] at this
  simp only [add_assoc, add_right_inj] at this
  simp only [← add_assoc, add_left_inj] at this
  simpa only [← two_mul] using this

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