inductive
definition
BaseQuantity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.DimensionalAnalysisFromConfigDim on GitHub at line 19.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
16
17namespace IndisputableMonolith.Physics.DimensionalAnalysisFromConfigDim
18
19inductive BaseQuantity where
20 | length
21 | mass
22 | time
23 | electricCurrent
24 | temperature
25 deriving DecidableEq, Repr, BEq, Fintype
26
27theorem baseQuantity_count : Fintype.card BaseQuantity = 5 := by decide
28
29/-- 7 SI base quantities; 5 primary + 2 derived. -/
30theorem si_partition : (7 : ℕ) = 5 + 2 := by decide
31
32structure DimensionalAnalysisCert where
33 five_primary : Fintype.card BaseQuantity = 5
34 si_split : (7 : ℕ) = 5 + 2
35
36def dimensionalAnalysisCert : DimensionalAnalysisCert where
37 five_primary := baseQuantity_count
38 si_split := si_partition
39
40end IndisputableMonolith.Physics.DimensionalAnalysisFromConfigDim