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)

  24inductive NumberSystem where
  25  | natural | integer | rational | real | complex
  26  deriving DecidableEq, Repr, BEq, Fintype
  27

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

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

Lean names referenced from this declaration's body.

NumberSystem in IndisputableMonolith.Mathematics.ElementaryRegularNumberSystems decl_use