Statement file: latticeShift (Roots). This file contains exactly one declaration of the formalization's public statement surface.

def AVenhance.latticeShift (n : Fin 2 → ℤ) : Homogenization.Vec 2

Integer translation x ↦ x + n on Vec 2.

Equations

• AVenhance.latticeShift n i = ↑(n i)