OAI/Combinatorics/PolynomialVacuum/Algebra/NaturalCovariance.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.PolynomialVacuumAlgebra.NatSpectralTensorline 9 - def
OAI.PolynomialVacuumAlgebra.LowerExchangeline 11 - def
OAI.PolynomialVacuumAlgebra.naturalPrescriptionline 15 - theorem
OAI.PolynomialVacuumAlgebra.naturalPrescription_swap_beforeline 20 - theorem
OAI.PolynomialVacuumAlgebra.naturalPrescription_swap_afterline 45 - theorem
OAI.PolynomialVacuumAlgebra.naturalPrescription_mark_rightline 69