theorem
proved
semiconductorDeviceCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.SemiconductorPhysicsFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | diode | bjt | mosfet | jfet | igbt
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem semiconductorDeviceCount : Fintype.card SemiconductorDevice = 5 := by decide
29
30/-- 2 carrier types = D - 1. -/
31def carrierTypes : ℕ := 2
32theorem carrierTypes_eq_Dminus1 : carrierTypes = 3 - 1 := by decide
33
34/-- 8 crystal symmetry operations = 2^D. -/
35def crystalSymmetries : ℕ := 2 ^ 3
36theorem crystalSymmetries_8 : crystalSymmetries = 8 := by decide
37
38structure SemiconductorPhysicsCert where
39 five_devices : Fintype.card SemiconductorDevice = 5
40 two_carriers : carrierTypes = 3 - 1
41 eight_syms : crystalSymmetries = 8
42
43def semiconductorPhysicsCert : SemiconductorPhysicsCert where
44 five_devices := semiconductorDeviceCount
45 two_carriers := carrierTypes_eq_Dminus1
46 eight_syms := crystalSymmetries_8
47
48end IndisputableMonolith.Physics.SemiconductorPhysicsFromRS