English
Reflecting reflective vectors again preserves reflectivity, and the reflected vector remains reflective with respect to the same bilinear form.
Русский
Повторное отражение отражательных векторов сохраняет отражаемость и сохраняет ту же билинейную форму.
LaTeX
$$reflective_reflection (hSB) hx hy : IsReflective B (Module.reflection (coroot_apply_self B hx) y)$$
Lean4
theorem reflective_reflection (hSB : LinearMap.IsSymm B) {y : M} (hx : IsReflective B x) (hy : IsReflective B y) :
IsReflective B (Module.reflection (coroot_apply_self B hx) y) :=
by
constructor
· rw [isOrthogonal_reflection B hx hSB]
exact hy.1
· intro z
have hz : Module.reflection (coroot_apply_self B hx) (Module.reflection (coroot_apply_self B hx) z) = z := by
exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl
rw [← hz, isOrthogonal_reflection B hx hSB, isOrthogonal_reflection B hx hSB]
exact hy.2 _
