structure
definition
SolidStatePhysicsCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.SolidStatePhysicsFromRS on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
32
33noncomputable def bandGap (k : ℕ) : ℝ := phi ^ k
34
35structure SolidStatePhysicsCert where
36 five_phenomena : Fintype.card SolidStatePhenomenon = 5
37 eight_kpoints : brillouinKPoints = 8
38
39def solidStatePhysicsCert : SolidStatePhysicsCert where
40 five_phenomena := solidStatePhenomenonCount
41 eight_kpoints := brillouinKPoints_8
42
43end IndisputableMonolith.Physics.SolidStatePhysicsFromRS