Theorems · Theorem · linear algebra

Module.reflection_mul_reflection_pow_apply

∀ {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 : ℕ) (z : M) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_pow_apply._auto_1 →
    ((Module.reflection hf * Module.reflection hg) ^ m) z =
      z +
          (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)) *
              (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) +
                Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m / 2)) +
              Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)

A formula for $(r_1 r_2)^m z$, where $m$ is a natural number and $z \in M$.

Defined in

Mathlib.LinearAlgebra.Reflection

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule