32.1. Keystones🔗

exists_periodLattice_realBasis — source · report an issue

theorem exists_periodLattice_realBasis :
    ∃ b : Module.Basis (Fin (2 * genus X)) ℝ (Fin (genus X) → ℂ),
      truePeriodLattice X = Submodule.span ℤ (Set.range ⇑b)