Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr

Equations
  • One or more equations did not get rendered due to their size.

Returns some c, where c is an equation from the basis whose leading monomial divides m. Remark: if the current ring does not satisfy the property

∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0

then the leading coefficient of the equation must also divide k

Equations
  • One or more equations did not get rendered due to their size.
Equations

Returns some c, where c is an equation from the basis whose leading monomial divides some monomial in p.

Equations

Simplifies d.p using c, and returns an extended polynomial derivation.

Equations
  • One or more equations did not get rendered due to their size.

Simplified d.p using the current basis, and returns the extended polynomial derivation.

Equations
  • One or more equations did not get rendered due to their size.

Simplifies c₁ using c₂.

Equations
  • One or more equations did not get rendered due to their size.

Simplifies c₁ using c₂.

Equations

Simplifies c₁ using c₂ exhaustively.

Simplify the given equation constraint using the current basis.

Equations
  • One or more equations did not get rendered due to their size.

Returns true if c.p is the constant polynomial.

Equations
  • One or more equations did not get rendered due to their size.

Simplifies and checks whether the resulting constraint is trivial (i.e., 0 = 0), or inconsistent (i.e., k = 0 where k % c != 0 for a comm-ring with characteristic c), and returns none. Otherwise, returns the simplified constraint.

Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

Tries to convert the leading monomial into a monic one.

It exploits the fact that given a polynomial with leading coefficient k, if the ring has a nonzero characteristic p and gcd k p = 1, then k has an inverse.

It also handles the easy case where k is -1.

Remark: if the ring implements the class NoNatZeroDivisors, then the coefficients are divided by the gcd of all coefficients.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.

Returns true if c.d.p is the constant polynomial.

Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_process_ring_eq]
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_process_ring_diseq]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.