theorem proved term proof

`bcc_packing_lt_fcc`

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

formal statement (Lean)

  73theorem bcc_packing_lt_fcc : packingEfficiencyApprox .BCC < packingEfficiencyApprox .FCC := by

Term-mode proof.

  74  simp only [packingEfficiencyApprox]
  75  norm_num
  76
  77/-- FCC and HCP have same packing. -/

Lean names referenced from this declaration's body.

packingEfficiencyApprox in IndisputableMonolith.Chemistry.CrystalStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use