LeanPool.Rupert.Icosahedron

Imported Lean Pool material for LeanPool.Rupert.Icosahedron.

noncomputable def Icosahedron.icosahedron : Fin 12 → ℝ³

The twelve vertices of a regular icosahedron in ℝ³.

Equations

• One or more equations did not get rendered due to their size.