inductive definition def or abbrev

`Sign`

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

formal statement (Lean)

  65inductive Sign : Type
  66  | neg : Sign
  67  | zero : Sign
  68  | pos : Sign
  69  deriving DecidableEq, Repr
  70
  71/-- Sign is nonempty -/
  72instance : Nonempty Sign := ⟨Sign.zero⟩

proof body

Definition body.

  73
  74/-- The sign function -/

used by (13)

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

argon_ea_zero in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
halogenZ in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
BandingFalsifier in IndisputableMonolith.Flight.Falsifiers decl_use
axis_perm_count_D3 in IndisputableMonolith.Foundation.GaugeFromCube decl_use
sign_flip_count_D3 in IndisputableMonolith.Foundation.GaugeFromCube decl_use
CoherenceGateFalsifier in IndisputableMonolith.Gravity.Candidates.Li decl_use
Jcost_pos_away_from_one in IndisputableMonolith.Information.LocalCache decl_use
composition_refines in IndisputableMonolith.RecogGeom.Examples decl_use
diff_magnitude_dist in IndisputableMonolith.RecogGeom.Examples decl_use
discrete_singleton_cells in IndisputableMonolith.RecogGeom.Examples decl_use
examples_status in IndisputableMonolith.RecogGeom.Examples decl_use
signOf in IndisputableMonolith.RecogGeom.Examples decl_use
signRecognizer in IndisputableMonolith.RecogGeom.Examples decl_use

depends on (9)

Lean names referenced from this declaration's body.

neg in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
neg in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
neg in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
neg in IndisputableMonolith.Numerics.Interval.Basic decl_use
neg in IndisputableMonolith.RecogSpec.Core decl_use