OAI/Geometry/UnitDistances/Derivations.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarUnitDistances.BivariateDegree.coeff_swap line 10
  2. lemma OAI.PlanarUnitDistances.BivariateDegree.coeff_natDegree_le_swap line 22
  3. def OAI.PlanarUnitDistances.BivariateDegree.size line 32
  4. lemma OAI.PlanarUnitDistances.BivariateDegree.size_mul line 34
  5. lemma OAI.PlanarUnitDistances.BivariateDegree.size_eq_zero_iff line 42
  6. lemma OAI.PlanarUnitDistances.BivariateDegree.size_pos_iff line 57
  7. lemma OAI.PlanarUnitDistances.BivariateDegree.size_le_of_dvd line 69
  8. theorem OAI.PlanarUnitDistances.BivariateDegree.irreducible_zero_capture line 76
  9. lemma OAI.PlanarUnitDistances.BiAffine.expansion line 123
  10. lemma OAI.PlanarUnitDistances.BiAffine.linear_not_unit line 135
  11. lemma OAI.PlanarUnitDistances.BiAffine.determinant_ne_zero line 140
  12. theorem OAI.PlanarUnitDistances.BiAffine.line_or_circle line 166
  13. lemma OAI.PlanarUnitDistances.CurveSeparation.resultant_ne_zero line 238
  14. theorem OAI.PlanarUnitDistances.CurveSeparation.eval_ne_zero line 255
  15. lemma OAI.PlanarUnitDistances.BivariateMaps.eval_transport line 275
  16. theorem OAI.PlanarUnitDistances.Radicals.curve_locus_differential_obstruction line 296
  17. def OAI.UnitDistances.DerivationObstruction.extendDerivation line 369
  18. theorem OAI.UnitDistances.DerivationObstruction.extendDerivation_algebraMap line 374
  19. theorem OAI.UnitDistances.DerivationObstruction.exists_derivation_basis_one line 384
  20. theorem OAI.UnitDistances.DerivationObstruction.exists_derivation_one line 421
  21. theorem OAI.UnitDistances.DerivationObstruction.exists_common_derivation line 429
  22. theorem OAI.PlanarUnitDistances.GridDerivation.exists_derivation_log line 450
  23. lemma OAI.UnitDistanceSurvival.free_subset line 477
  24. lemma OAI.UnitDistanceSurvival.surviving_block line 507
  25. lemma OAI.UnitDistanceSurvival.independent_over_basis line 539
  26. theorem OAI.UnitDistanceSurvival.survives_algebraic_closure line 604