OAI/Combinatorics/PolynomialVacuum/Algebra/AnalyticResolvent.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.vacuumResolventline 11 - def
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.normalizedVacuumline 13 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.vacuumResolvent_oneline 16 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.vacuumResolvent_det_ne_zeroline 20 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.analytic_vacuumResolventline 36 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.analytic_normalizedVacuumline 43 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.vacuumResolvent_eventually_ne_zeroline 48 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.resolvent_fixed_relationline 52 - theorem
OAI.PolynomialVacuumAlgebra.AnalyticVacuum.normalizedVacuum_eq_ratioline 63