isOrthogonal_reflection — Mathlib

English

If B is symmetric, the reflection is an orthogonal transformation with respect to B.

Русский

Если B симметрична, отражение является ортогональным преобразованием относительно B.

LaTeX

$$isOrthogonal_reflection (B) (hx) : B.IsOrthogonal (Module.reflection (coroot_apply_self B hx))$$

Lean4

theorem isOrthogonal_reflection (hSB : LinearMap.IsSymm B) :
    B.IsOrthogonal (Module.reflection (coroot_apply_self B hx)) :=
  by
  intro y z
  simp only [reflection_apply, LinearMap.map_sub, map_smul, sub_apply, smul_apply, smul_eq_mul]
  refine hx.1.1 ?_
  simp only [mul_sub, ← mul_assoc, apply_self_mul_coroot_apply]
  rw [sub_eq_iff_eq_add, ← hSB.eq x y, RingHom.id_apply, mul_assoc _ _ (B x x), mul_comm _ (B x x),
    apply_self_mul_coroot_apply]
  ring

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