OAI/Combinatorics/PolynomialVacuum/Algebra/NaturalCup.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PolynomialVacuumAlgebra.skipTwoline 9 - def
OAI.PolynomialVacuumAlgebra.skipOneline 12 - def
OAI.PolynomialVacuumAlgebra.cupLinearline 15 - theorem
OAI.PolynomialVacuumAlgebra.skipTwo_beforeline 20 - theorem
OAI.PolynomialVacuumAlgebra.skipTwo_afterline 26 - theorem
OAI.PolynomialVacuumAlgebra.skipTwo_slidingline 32 - theorem
OAI.PolynomialVacuumAlgebra.skipTwo_slide_endline 39 - theorem
OAI.PolynomialVacuumAlgebra.siteR_cup_beforeline 45 - theorem
OAI.PolynomialVacuumAlgebra.siteR_cup_afterline 60 - theorem
OAI.PolynomialVacuumAlgebra.siteR_cup_slideline 77