OAI/Analysis/SymmetricDomains/AnalyticNashRank.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Release061.nash_partial_span_rank_eq_trdegline 34 - def
OAI.Release061.meromorphicGermOfline 74 - theorem
OAI.Release061.meromorphicGermOf_eq_zero_iffline 78 - def
OAI.Release061.meromorphicPartialline 84 - theorem
OAI.Release061.meromorphicPartial_coordinateline 88 - theorem
OAI.Release061.meromorphicGerm_aeval_eq_zero_iffline 95 - theorem
OAI.Release061.analytic_nash_polynomial_relationline 116 - theorem
OAI.Release061.analytic_nash_rankline 140