OAI/AlgebraicGeometry/Seshadri/Lattice/NodePolygon.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.NodalLocal.bivariateCoeff line 13
  2. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_x line 16
  3. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_z line 20
  4. def OAI.MaximalSeshadri.NodalLocal.bivariateCoeffEquiv line 24
  5. theorem OAI.MaximalSeshadri.NodalLocal.nodal_initial_weight_bound line 37
  6. theorem OAI.MaximalSeshadri.NodalLocal.residual_initial_weight_bound line 61
  7. lemma OAI.MaximalSeshadri.NodalLocal.exponentWeight_add line 78
  8. lemma OAI.MaximalSeshadri.NodalLocal.exponentWeight_pos line 83
  9. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_mul line 96
  10. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_eq_zero_of_weight_lt line 102
  11. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_eq_zero_of_proper_subterm line 108
  12. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_mul_of_weight_le line 118
  13. theorem OAI.MaximalSeshadri.NodalLocal.lexInitial_unit_mul line 157
  14. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_node_pow_mul line 170
  15. lemma OAI.MaximalSeshadri.NodalLocal.bivariateCoeff_node_pow_mul_add line 181
  16. theorem OAI.MaximalSeshadri.NodalLocal.lexInitial_node_pow_mul line 185
  17. theorem OAI.MaximalSeshadri.NodalLocal.lexInitial_nodal_factor line 210
  18. def OAI.MaximalSeshadri.nodeQuadrilateral line 228
  19. theorem OAI.MaximalSeshadri.mem_nodeQuadrilateral_of_residual line 231
  20. theorem OAI.MaximalSeshadri.NodalLocal.nodal_factor_quadrilateral line 266