def
definition
topological_phases_from_ledger
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CondensedMatter.TopologicalPhasesStructure on GitHub at line 10.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
7
8open StronglyCorrelatedElectronsStructure
9
10def topological_phases_from_ledger : Prop := strongly_correlated_electrons_from_ledger
11
12theorem topological_phases_structure : topological_phases_from_ledger :=
13 strongly_correlated_electrons_structure
14
15/-- Topological-phase structure implies strongly-correlated-electron input. -/
16theorem topological_phases_implies_strongly_correlated (h : topological_phases_from_ledger) :
17 strongly_correlated_electrons_from_ledger :=
18 h
19
20end TopologicalPhasesStructure
21end CondensedMatter
22end IndisputableMonolith