`IndisputableMonolith.CondensedMatter.StronglyCorrelatedElectronsStructure`

IndisputableMonolith/CondensedMatter/StronglyCorrelatedElectronsStructure.lean · 23 lines · 3 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.CondensedMatter.GlassTransitionStructure
   3
   4namespace IndisputableMonolith
   5namespace CondensedMatter
   6namespace StronglyCorrelatedElectronsStructure
   7
   8open GlassTransitionStructure
   9
  10def strongly_correlated_electrons_from_ledger : Prop := glass_transition_from_ledger
  11
  12theorem strongly_correlated_electrons_structure :
  13    strongly_correlated_electrons_from_ledger := glass_transition_structure
  14
  15/-- Strong-correlation structure implies glass-transition structural input. -/
  16theorem strongly_correlated_implies_glass (h : strongly_correlated_electrons_from_ledger) :
  17    glass_transition_from_ledger :=
  18  h
  19
  20end StronglyCorrelatedElectronsStructure
  21end CondensedMatter
  22end IndisputableMonolith
  23

source mirrored from github.com/jonwashburn/shape-of-logic