inductive
definition
NumberSystem
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.ElementaryRegularNumberSystems on GitHub at line 18.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
15
16namespace IndisputableMonolith.Mathematics.ElementaryRegularNumberSystems
17
18inductive NumberSystem where
19 | naturals
20 | integers
21 | rationals
22 | reals
23 | complexes
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem numberSystem_count : Fintype.card NumberSystem = 5 := by decide
27
28structure NumberSystemCert where
29 five_systems : Fintype.card NumberSystem = 5
30
31def numberSystemCert : NumberSystemCert where
32 five_systems := numberSystem_count
33
34end IndisputableMonolith.Mathematics.ElementaryRegularNumberSystems