OAI/RepresentationTheory/RestrictedTilting/LowDegreeTrace.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.FiberFunctorProof.additive_lagrange_denominatorline 12 - theorem
OAI.FiberFunctorProof.finite_additive_polynomial_sum_zeroline 24 - lemma
OAI.FiberFunctorProof.finite_additive_power_sum_zeroline 44