theorem
proved
has_high_tc_structure
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CondensedMatter.RoomTemperatureSuperconductivityStructure on GitHub at line 10.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
7
8open HighTcSuperconductivityStructure
9
10theorem has_high_tc_structure : high_tc_superconductivity_from_ledger :=
11 high_tc_superconductivity_structure
12
13def room_temperature_superconductivity_from_ledger : Prop :=
14 high_tc_superconductivity_from_ledger
15
16theorem room_temperature_superconductivity_structure :
17 room_temperature_superconductivity_from_ledger := has_high_tc_structure
18
19/-- Room-temperature-SC structure implies High-Tc structural input. -/
20theorem room_temperature_implies_high_tc (h : room_temperature_superconductivity_from_ledger) :
21 high_tc_superconductivity_from_ledger :=
22 h
23
24end RoomTemperatureSuperconductivityStructure
25end CondensedMatter
26end IndisputableMonolith