OAI/RepresentationTheory/RestrictedTilting/LaurentPolynomialSeparation.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.FiberFunctorProof.polynomial_eq_of_base_evalsline 10 - lemma
OAI.FiberFunctorProof.laurent_eq_zero_of_base_evalsline 17 - lemma
OAI.FiberFunctorProof.laurent_eq_of_base_evalsline 38 - lemma
OAI.FiberFunctorProof.laurent_eq_of_evalsline 46