def definition def or abbrev

`fourColorCert`

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

formal statement (Lean)

  41def fourColorCert : FourColorCert where
  42  four_eq_Dp1 := fourColors_eq_DplusOne

Definition body.

  43  four_eq_2sq := fourColors_eq_2sq
  44  f2sq := four_eq_F2sq
  45
  46end IndisputableMonolith.Mathematics.FourColorTheoremFromRS

Lean names referenced from this declaration's body.

FourColorCert in IndisputableMonolith.Mathematics.FourColorTheoremFromRS decl_use
fourColors_eq_2sq in IndisputableMonolith.Mathematics.FourColorTheoremFromRS decl_use
fourColors_eq_DplusOne in IndisputableMonolith.Mathematics.FourColorTheoremFromRS decl_use
four_eq_F2sq in IndisputableMonolith.Mathematics.FourColorTheoremFromRS decl_use