OAI/RepresentationTheory/UniversalSquare/Contraction/PolynomialDetection.lean
11 declarations, 0 contain sorry, 0 declared as axioms
Polynomial Detection.
- def
OAI.Saxl.jointContentline 15 - lemma
OAI.Saxl.jointContent_applyline 18 - lemma
OAI.Saxl.perm_of_equal_jointContentline 24 - lemma
OAI.Saxl.intertwiner_jointContentline 45 - def
OAI.Saxl.pairingPolynomialline 70 - lemma
OAI.Saxl.eval_jointContent_monomialline 74 - lemma
OAI.Saxl.pairingPolynomial_evalline 89 - def
OAI.Saxl.jointContentWeightline 105 - lemma
OAI.Saxl.jointContentWeight_applyline 111 - lemma
OAI.Saxl.pairingPolynomial_zero_pairline 121 - theorem
OAI.Saxl.wordMap_detects_intertwinerline 150