theorem
proved
baseQuantity_count
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 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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