`high_tc_implies_phi_lt_two`

proved

show as: view math explainer →

module: IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure
domain: CondensedMatter
line: 20 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure on GitHub at line 20.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

high_tc_superconductivity_from_ledger IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure

formal source

  17  h.1
  18
  19/-- High-Tc structure implies upper bound `phi < 2`. -/
  20theorem high_tc_implies_phi_lt_two (h : high_tc_superconductivity_from_ledger) : phi < 2 :=
  21  h.2
  22
  23end HighTcSuperconductivityStructure
  24end CondensedMatter
  25end IndisputableMonolith

papers checked against this theorem

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