OAI/Combinatorics/Chromatic/GradedAlgebra/RealRootCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.coefficient_simple_expansion line 13
2. lemma OAI.ElementaryPositivity.QuantumTorus.realRootCoordinates_exists line 24
3. lemma OAI.ElementaryPositivity.QuantumTorus.covector_root_eval line 46
4. lemma OAI.ElementaryPositivity.QuantumTorus.real_coordinate_simple line 54