OAI/AlgebraicGeometry/AbhyankarSathaye/LinearElimination.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Elimination of compatible linear equations

A Bézout relation identifies the ideal of two compatible linear equations with a single evaluation relation, over any commutative ring.

  1. theorem OAI.AbhyankarSathaye.linear_ideal line 16
  2. def OAI.AbhyankarSathaye.linear_equations_quotient_equiv line 45