English
For h with f x = 2, reflection h applied to x equals −x, i.e., reflection(h)(x) = −x.
Русский
При h с f x = 2 отображение reflection h на вектор x даёт −x, то есть reflection(h)(x) = −x.
LaTeX
$$$\\text{If }h:\\ f(x)=2,\\ reflection(h)(x)= -x.$$$
Lean4
/-- Composite of reflections in "parallel" hyperplanes is a shear (special case). -/
theorem reflection_reflection_iterate (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) (n : ℕ) :
((reflection hgy).trans (reflection hfx))^[n] y = y + n • (f y • x - (2 : R) • y) := by
induction n with
| zero => simp
| succ n
ih =>
have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
intro z
rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl, Nat.cast_ofNat]
simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add, LinearEquiv.trans_apply,
reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub, map_nsmul, map_smul, smul_neg, hz, add_smul]
abel
