def
definition
semiconductorCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.SemiconductorBandStructureFromConfigDim on GitHub at line 44.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
41 phi_ratio : ∀ k, bandGap (k + 1) / bandGap k = phi
42 bandGap_always_pos : ∀ k, 0 < bandGap k
43
44noncomputable def semiconductorCert : SemiconductorCert where
45 five_types := semiconductorType_count
46 phi_ratio := bandGap_ratio
47 bandGap_always_pos := bandGap_pos
48
49end IndisputableMonolith.Physics.SemiconductorBandStructureFromConfigDim