theorem
proved
numberSystemCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.NumberSystemsFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | natural | integer | rational | real | complex
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem numberSystemCount : Fintype.card NumberSystem = 5 := by decide
29
30/-- Rational system contains J-cost domain (positive rationals). -/
31theorem rational_contains_jcost_domain : (1 : ℚ) > 0 := by norm_num
32
33structure NumberSystemCert where
34 five_systems : Fintype.card NumberSystem = 5
35 rational_pos : (1 : ℚ) > 0
36
37def numberSystemCert : NumberSystemCert where
38 five_systems := numberSystemCount
39 rational_pos := rational_contains_jcost_domain
40
41end IndisputableMonolith.Mathematics.NumberSystemsFromRS