Documentation

LeanPool.HopfProblem.Uniformization.CuspUniformization4

Hopf problem: uniformization · cusp uniformization 4 #

Supporting definitions and proofs for this stage of the six-sphere construction.

source
def Mathoverflow1973.SpecialPeriods.triangleLatticeMulAutHom :
TriangleGroup →* MulAut (Multiplicative Lattice)

The triangle-group action by multiplicative automorphisms of the lattice.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Mathoverflow1973.SpecialPeriods.triangleLatticeMulAutHom_toAdd (g : TriangleGroup) (n : Multiplicative Lattice) :
    Multiplicative.toAdd ((triangleLatticeMulAutHom g) n) = (↑(triangleDualRepresentation g)).mulVec (Multiplicative.toAdd n)