Theorems · Theorem · linear algebra

Module.reflection_mul_reflection_zpow_apply_self

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_zpow_apply_self._auto_1 →
    ((Module.reflection hf * Module.reflection hg) ^ m) x =
      (Polynomial.eval t (Polynomial.Chebyshev.S R m) + Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1))) • x +
        (Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1)) * -g x) • y

A formula for $(r_1 r_2)^m x$, where $m$ is an integer. This is the special case of Module.reflection_mul_reflection_zpow_apply with $z = x$.

Defined in

Mathlib.LinearAlgebra.Reflection

Cited by

2 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule