OAI/Algebra/AffineCancellation/BundleGrading.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComplexCancellation.Bundle.fiberEuler_j line 10
2. lemma OAI.ComplexCancellation.Bundle.fiberEuler_τ line 11
3. lemma OAI.ComplexCancellation.Bundle.fiberEuler_V line 12
4. lemma OAI.ComplexCancellation.Bundle.j_mem line 13
5. lemma OAI.ComplexCancellation.Bundle.τ_mem line 14
6. lemma OAI.ComplexCancellation.Bundle.V_mem line 15
7. lemma OAI.ComplexCancellation.Bundle.fiberEuler_homogeneous line 16
8. lemma OAI.ComplexCancellation.Bundle.pullback_graded line 33