LeanPool.Rupert.SnubCube

Imported Lean Pool material for LeanPool.Rupert.SnubCube.

@[reducible, inline]

noncomputable abbrev SnubCube.cbrt (x : ℝ) : ℝ

Real cube root, written using real powers.

Equations

• SnubCube.cbrt x = x ^ (1 / 3)

noncomputable def SnubCube.trib : ℝ

tribonacci constant

Equations

• SnubCube.trib = (1 + SnubCube.cbrt (19 + 3 * √33) + SnubCube.cbrt (19 - 3 * √33)) / 3

noncomputable def SnubCube.snubCube : Fin 24 → ℝ³

Coordinates for a snub cube.

Equations

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