Powers of Eichler transvections #
Powers of E_{u,w} are obtained by multiplying its parameter by the exponent. This is the
one-parameter subgroup law of QuadraticMap.transvectionHom, read on representatives. In
particular, the nonnegative powers of a rational transvection have uniformly controlled
integrality at finite places.
@[simp]
theorem
TauCeti.QuadraticMap.transvection_pow
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{u w : M}
(hu : Q u = 0)
(huw : QuadraticMap.polar (⇑Q) u w = 0)
(n : ℕ)
:
The nth power of an Eichler transvection is the transvection with parameter n • w.