def definition def or abbrev

`packingEfficiency`

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

formal statement (Lean)

  54def packingEfficiency : Structure → ℝ
  55| .BCC => Real.pi * Real.sqrt 3 / 8  -- ≈ 0.68
  56| .FCC => Real.pi / (3 * Real.sqrt 2) -- ≈ 0.74
  57| .HCP => Real.pi / (3 * Real.sqrt 2) -- ≈ 0.74
  58
  59/-- Approximate packing efficiency values. -/

used by (2)

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

fcc_hcp_denser_than_bcc in IndisputableMonolith.Chemistry.MetallicBond decl_use
packingEfficiency in IndisputableMonolith.Chemistry.MetallicBond decl_use

depends on (2)

Lean names referenced from this declaration's body.

Structure in IndisputableMonolith.Chemistry.CrystalStructure decl_use
packingEfficiency in IndisputableMonolith.Chemistry.MetallicBond decl_use