`graphTheoryDepthCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.GraphTheoryDepthFromRS
domain: Mathematics
line: 44 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.GraphTheoryDepthFromRS on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  41  euler_q3 : q3EulerChar = 2
  42  chromatic_q3 : q3ChromaticNumber = 2
  43
  44def graphTheoryDepthCert : GraphTheoryDepthCert where
  45  five_theorems := graphTheoremCount
  46  euler_q3 := q3Euler_eq_2
  47  chromatic_q3 := q3Chromatic_bipartite
  48
  49end IndisputableMonolith.Mathematics.GraphTheoryDepthFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.