pith. machine review for the scientific record. sign in
theorem proved term proof

deficit_eq_zero_of_flat

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 138theorem deficit_eq_zero_of_flat (ds : List DihedralAngleData)
 139    (h : FlatSumCondition ds) : deficit ds = 0 := by

proof body

Term-mode proof.

 140  unfold deficit
 141  rw [h]; ring
 142
 143/-- Four cube-dihedral angles (`π/2 + π/2 + π/2 + π/2 = 2π`) sum to `2π`:
 144    the classical "Z³ lattice is flat" statement. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.