OAI/RepresentationTheory/UniversalSquare/Contraction/FactoredCertificates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Factored Certificates.

  1. def OAI.Saxl.Columns.integralWedge line 14
  2. def OAI.Saxl.Columns.integralBlocks line 17
  3. lemma OAI.Saxl.Columns.integralBlocks_eq line 22
  4. def OAI.Saxl.Columns.factoredContraction line 64
  5. lemma OAI.Saxl.Columns.contractionInteger_eq_factored line 72