inductive definition def or abbrev

`NumberSystem`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  18inductive NumberSystem where
  19  | naturals
  20  | integers
  21  | rationals
  22  | reals
  23  | complexes
  24  deriving DecidableEq, Repr, BEq, Fintype
  25

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

NumberSystemCert in IndisputableMonolith.Mathematics.ElementaryRegularNumberSystems decl_use
numberSystem_count in IndisputableMonolith.Mathematics.ElementaryRegularNumberSystems decl_use
NumberSystem in IndisputableMonolith.Mathematics.NumberSystemsFromRS decl_use
NumberSystemCert in IndisputableMonolith.Mathematics.NumberSystemsFromRS decl_use
numberSystemCount in IndisputableMonolith.Mathematics.NumberSystemsFromRS decl_use

depends on (1)

Lean names referenced from this declaration's body.

NumberSystem in IndisputableMonolith.Mathematics.NumberSystemsFromRS decl_use