ring tactic

A tactic for solving equations in commutative (semi)rings, where the exponents can also contain variables. Based on http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf .

More precisely, expressions of the following form are supported:

• constants (non-negative integers)
• variables
• coefficients (any rational number, embedded into the (semi)ring)
• addition of expressions
• multiplication of expressions (a * b)
• scalar multiplication of expressions (n • a; the multiplier must have type ℕ)
• exponentiation of expressions (the exponent must have type ℕ)
• subtraction and negation of expressions (if the base is a full ring)

The extension to exponents means that something like 2 * 2^n * b = b * 2^(n+1) can be proved, even though it is not strictly speaking an equation in the language of commutative rings.

Implementation notes

The basic approach to prove equalities is to normalise both sides and check for equality. The normalisation is guided by building a value in the type ExSum at the meta level, together with a proof (at the base level) that the original value is equal to the normalised version.

The outline of the file:

• Define a mutual inductive family of types ExSum, ExProd, ExBase, which can represent expressions with +, *, ^ and rational numerals. The mutual induction ensures that associativity and distributivity are applied, by restricting which kinds of subexpressions appear as arguments to the various operators.
• Represent addition, multiplication and exponentiation in the ExSum type, thus allowing us to map expressions to ExSum (the eval function drives this). We apply associativity and distributivity of the operators here (helped by Ex* types) and commutativity as well (by sorting the subterms; unfortunately not helped by anything). Any expression not of the above formats is treated as an atom (the same as a variable).

There are some details we glossed over which make the plan more complicated:

• The order on atoms is not initially obvious. We construct a list containing them in order of initial appearance in the expression, then use the index into the list as a key to order on.
• For pow, the exponent must be a natural number, while the base can be any semiring α. We swap out operations for the base ring α with those for the exponent ring ℕ as soon as we deal with exponents.

Caveats and future work

The normalized form of an expression is the one that is useful for the tactic, but not as nice to read. To remedy this, the user-facing normalization calls ringNFCore.

Subtraction cancels out identical terms, but division does not. That is: a - a = 0 := by ring solves the goal, but a / a := 1 by ring doesn't. Note that 0 / 0 is generally defined to be 0, so division cancelling out is not true in general.

Multiplication of powers can be simplified a little bit further: 2 ^ n * 2 ^ n = 4 ^ n := by ring could be implemented in a similar way that 2 * a + 2 * a = 4 * a := by ring already works. This feature wasn't needed yet, so it's not implemented yet.

Tags

ring, semiring, exponent, power

ink

instance instOrdRat : Ord ℚ

Equations

• instOrdRat = { compare := fun x y => compareOfLessAndEq x y }

ink

def Mathlib.Tactic.Ring.instCommSemiringNat : CommSemiring ℕ

A shortcut instance for CommSemiring ℕ used by ring.

Equations

• Mathlib.Tactic.Ring.instCommSemiringNat = inferInstance

ink

def Mathlib.Tactic.Ring.sℕ : Q(CommSemiring ℕ)

A typed expression of type CommSemiring ℕ used when we are working on ring subexpressions of type ℕ.

Equations

• Mathlib.Tactic.Ring.sℕ = q(Mathlib.Tactic.Ring.instCommSemiringNat)

ink

inductive Mathlib.Tactic.Ring.ExBase {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α) → Qq.QQ α → Type

• An atomic expression e with id id.

  Atomic expressions are those which ring cannot parse any further. For instance, a + (a % b) has a and (a % b) as atoms. The ring1 tactic does not normalize the subexpressions in atoms, but ring_nf does.

  Atoms in fact represent equivalence classes of expressions, modulo definitional equality. The field index : ℕ should be a unique number for each class, while value : expr contains a representative of this class. The function resolve_atom determines the appropriate atom for a given expression.

  atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ℕ → Mathlib.Tactic.Ring.ExBase sα e

• A sum of monomials.

  sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.ExSum sα e → Mathlib.Tactic.Ring.ExBase sα e

The base e of a normalized exponent expression.

ink

inductive Mathlib.Tactic.Ring.ExProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α) → Qq.QQ α → Type

• A coefficient value, which must not be 0. e is a raw rat cast. If value is not an integer, then hyp should be a proof of (value.den : α) ≠ 0≠ 0.

  const: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ℚ → optParam (Option Lean.Expr) none → Mathlib.Tactic.Ring.ExProd sα e

• A product x ^ e * b is a monomial if b is a monomial. Here x is a ExBase and e is a ExProd representing a monomial expression in ℕ (it is a monomial instead of a polynomial because we eagerly normalize x ^ (a + b) = x ^ a * x ^ b.)

  mul: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {x : Q(«$α»)} → {e : Q(ℕ)} → {b : Q(«$α»)} → Mathlib.Tactic.Ring.ExBase sα x → Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ e → Mathlib.Tactic.Ring.ExProd sα b → Mathlib.Tactic.Ring.ExProd sα q(«$x» ^ «$e» * «$b»)

A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient.

ink

inductive Mathlib.Tactic.Ring.ExSum {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α) → Qq.QQ α → Type

• Zero is a polynomial. e is the expression 0.

  zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → Mathlib.Tactic.Ring.ExSum sα q(0)

• A sum a + b is a polynomial if a is a monomial and b is another polynomial.

  add: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {a b : Q(«$α»)} → Mathlib.Tactic.Ring.ExProd sα a → Mathlib.Tactic.Ring.ExSum sα b → Mathlib.Tactic.Ring.ExSum sα q(«$a» + «$b»)

A polynomial expression, which is a sum of monomials.

ink

partial def Mathlib.Tactic.Ring.ExBase.eq : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase sα a_1 → Mathlib.Tactic.Ring.ExBase sα b → Bool

Equality test for expressions. This is not a BEq instance because it is heterogeneous.

ink

partial def Mathlib.Tactic.Ring.ExProd.eq : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd sα a_1 → Mathlib.Tactic.Ring.ExProd sα b → Bool

Equality test for expressions. This is not a BEq instance because it is heterogeneous.

ink

partial def Mathlib.Tactic.Ring.ExSum.eq : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum sα a_1 → Mathlib.Tactic.Ring.ExSum sα b → Bool

Equality test for expressions. This is not a BEq instance because it is heterogeneous.

ink

partial def Mathlib.Tactic.Ring.ExBase.cmp : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase sα a_1 → Mathlib.Tactic.Ring.ExBase sα b → Ordering

A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

ink

partial def Mathlib.Tactic.Ring.ExProd.cmp : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd sα a_1 → Mathlib.Tactic.Ring.ExProd sα b → Ordering

A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

ink

partial def Mathlib.Tactic.Ring.ExSum.cmp : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum sα a_1 → Mathlib.Tactic.Ring.ExSum sα b → Ordering

A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

ink

instance Mathlib.Tactic.Ring.instInhabitedSigmaQQExBase : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExBase sα e)

Equations

• Mathlib.Tactic.Ring.instInhabitedSigmaQQExBase = { default := { fst := default, snd := Mathlib.Tactic.Ring.ExBase.atom 0 } }

ink

instance Mathlib.Tactic.Ring.instInhabitedSigmaQQExSum : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExSum sα e)

Equations

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

ink

instance Mathlib.Tactic.Ring.instInhabitedSigmaQQExProd : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExProd sα e)

Equations

• Mathlib.Tactic.Ring.instInhabitedSigmaQQExProd = { default := { fst := default, snd := Mathlib.Tactic.Ring.ExProd.const 0 } }

ink

partial def Mathlib.Tactic.Ring.ExBase.cast : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExBase sα a_1 → (a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExBase sβ a

Converts ExBase sα to ExBase sβ, assuming sα and sβ are defeq.

ink

partial def Mathlib.Tactic.Ring.ExProd.cast : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExProd sα a_1 → (a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExProd sβ a

Converts ExProd sα to ExProd sβ, assuming sα and sβ are defeq.

ink

partial def Mathlib.Tactic.Ring.ExSum.cast : {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExSum sα a_1 → (a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExSum sβ a

Converts ExSum sα to ExSum sβ, assuming sα and sβ are defeq.

ink

structure Mathlib.Tactic.Ring.Result {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (E : Qq.QQ α → Type) (e : Qq.QQ α) : Type

• The normalized result.

  expr : Qq.QQ α

• The data associated to the normalization.

  val : E expr

• A proof that the original expression is equal to the normalized result.

  proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Eq [Lean.Level.succ u]) α) e) expr)

The result of evaluating an (unnormalized) expression e into the type family E (one of ExSum, ExProd, ExBase) is a (normalized) element e' and a representation E e' for it, and a proof of e = e'.

ink

instance Mathlib.Tactic.Ring.instInhabitedResult : {a : Lean.Level} → {α : Q(Type a)} → {E : Q(«$α») → Type} → {e : Q(«$α»)} → [inst : Inhabited ((e : Q(«$α»)) × E e)] → Inhabited (Mathlib.Tactic.Ring.Result E e)

Equations

• Mathlib.Tactic.Ring.instInhabitedResult = match default with | { fst := e', snd := v } => { default := { expr := e', val := v, proof := default } }

ink

def Mathlib.Tactic.Ring.ExProd.mkNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (n : ℕ) : (e : Qq.QQ α) × Mathlib.Tactic.Ring.ExProd sα e

Constructs the expression corresponding to .const n. (The .const constructor does not check that the expression is correct.)

Equations

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

ink

def Mathlib.Tactic.Ring.ExProd.mkNegNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α) → ℕ → (e : Qq.QQ α) × Mathlib.Tactic.Ring.ExProd sα e

Constructs the expression corresponding to .const (-n). (The .const constructor does not check that the expression is correct.)

Equations

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

ink

def Mathlib.Tactic.Ring.ExProd.mkRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α) → ℚ → Qq.QQ (Lean.Expr.const `Int []) → Qq.QQ (Lean.Expr.const `Nat []) → Lean.Expr → (e : Qq.QQ α) × Mathlib.Tactic.Ring.ExProd sα e

Constructs the expression corresponding to .const (-n). (The .const constructor does not check that the expression is correct.)

Equations

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

ink

def Mathlib.Tactic.Ring.ExBase.toProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)} {a : Qq.QQ α} {b : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExBase sα a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) : Mathlib.Tactic.Ring.ExProd sα (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b)) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.rawCast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddCommMonoidWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toAddCommMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))))) (Lean.Expr.lit (Lean.Literal.natVal 1)))))

Embed an exponent (a ExBase, ExProd pair) as a ExProd by multiplying by 1.

Equations

• Mathlib.Tactic.Ring.ExBase.toProd va vb = Mathlib.Tactic.Ring.ExProd.mul va vb (Mathlib.Tactic.Ring.ExProd.const 1)

ink

def Mathlib.Tactic.Ring.ExProd.toSum {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)} {e : Qq.QQ α} (v : Mathlib.Tactic.Ring.ExProd sα e) : Mathlib.Tactic.Ring.ExSum sα (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HAdd.hAdd [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Distrib.toAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toDistrib [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))))))) e) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [u]) α) (Lean.Expr.lit (Lean.Literal.natVal 0))) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Zero.toOfNat0 [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommMonoidWithZero.toZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toCommMonoidWithZero [u]) α) sα))))))

Embed ExProd in ExSum by adding 0.

Equations

• Mathlib.Tactic.Ring.ExProd.toSum v = Mathlib.Tactic.Ring.ExSum.add v Mathlib.Tactic.Ring.ExSum.zero

ink

def Mathlib.Tactic.Ring.ExProd.coeff {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)} {e : Qq.QQ α} : Mathlib.Tactic.Ring.ExProd sα e → ℚ

Get the leading coefficient of a ExProd.

ink

inductive Mathlib.Tactic.Ring.Overlap {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (e : Qq.QQ α) : Type

• The expression e (the sum of monomials) is equal to 0.

  zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Q(Mathlib.Meta.NormNum.IsNat «$e» 0) → Mathlib.Tactic.Ring.Overlap sα e

• The expression e (the sum of monomials) is equal to another monomial (with nonzero leading coefficient).

  nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) e → Mathlib.Tactic.Ring.Overlap sα e

Two monomials are said to "overlap" if they differ by a constant factor, in which case the constants just add. When this happens, the constant may be either zero (if the monomials cancel) or nonzero (if they add up); the zero case is handled specially.

ink

theorem Mathlib.Tactic.Ring.add_overlap_pf {R : Type u_1} [inst : CommSemiring R] {a : R} {b : R} {c : R} (x : R) (e : ℕ) (pq_pf : a + b = c) : x ^ e * a + x ^ e * b = x ^ e * c

ink

theorem Mathlib.Tactic.Ring.add_overlap_pf_zero {R : Type u_1} [inst : CommSemiring R] {a : R} {b : R} (x : R) (e : ℕ) : Mathlib.Meta.NormNum.IsNat (a + b) 0 → Mathlib.Meta.NormNum.IsNat (x ^ e * a + x ^ e * b) 0

ink

def Mathlib.Tactic.Ring.evalAddOverlap {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExProd sα a) (vb : Mathlib.Tactic.Ring.ExProd sα b) : Option (Mathlib.Tactic.Ring.Overlap sα (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HAdd.hAdd [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Distrib.toAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toDistrib [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))))))) a) b)))

Given monomials va, vb, attempts to add them together to get another monomial. If the monomials are not compatible, returns none. For example, xy + 2xy = 3xy is a .nonzero overlap, while xy + xz returns none and xy + -xy = 0 is a .zero overlap.

ink

theorem Mathlib.Tactic.Ring.add_pf_zero_add {R : Type u_1} [inst : CommSemiring R] (b : R) : 0 + b = b

ink

theorem Mathlib.Tactic.Ring.add_pf_add_zero {R : Type u_1} [inst : CommSemiring R] (a : R) : a + 0 = a

ink

theorem Mathlib.Tactic.Ring.add_pf_add_overlap {R : Type u_1} [inst : CommSemiring R] {a₁ : R} {b₁ : R} {c₁ : R} {a₂ : R} {b₂ : R} {c₂ : R} : a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

ink

theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero {R : Type u_1} [inst : CommSemiring R] {a₁ : R} {b₁ : R} {a₂ : R} {b₂ : R} {c : R} (h : Mathlib.Meta.NormNum.IsNat (a₁ + b₁) 0) (h₄ : a₂ + b₂ = c) : a₁ + a₂ + (b₁ + b₂) = c

ink

theorem Mathlib.Tactic.Ring.add_pf_add_lt {R : Type u_1} [inst : CommSemiring R] {a₂ : R} {b : R} {c : R} (a₁ : R) : a₂ + b = c → a₁ + a₂ + b = a₁ + c

ink

theorem Mathlib.Tactic.Ring.add_pf_add_gt {R : Type u_1} [inst : CommSemiring R] {a : R} {b₂ : R} {c : R} (b₁ : R) : a + b₂ = c → a + (b₁ + b₂) = b₁ + c

ink

partial def Mathlib.Tactic.Ring.evalAdd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum sα a) (vb : Mathlib.Tactic.Ring.ExSum sα b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HAdd.hAdd [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Distrib.toAdd [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toDistrib [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))))))) a) b))

Adds two polynomials va, vb together to get a normalized result polynomial.

• 0 + b = 0
• a + 0 = 0
• a * x + a * y = a * (x + y) (for x, y coefficients; uses evalAddOverlap)
• (a₁ + a₂) + (b₁ + b₂) = a₁ + (a₂ + (b₁ + b₂)) (if a₁.lt b₁)
• (a₁ + a₂) + (b₁ + b₂) = b₁ + ((a₁ + a₂) + b₂) (if not a₁.lt b₁)

ink

theorem Mathlib.Tactic.Ring.one_mul {R : Type u_1} [inst : CommSemiring R] (a : R) : Nat.rawCast 1 * a = a

ink

theorem Mathlib.Tactic.Ring.mul_one {R : Type u_1} [inst : CommSemiring R] (a : R) : a * Nat.rawCast 1 = a

ink

theorem Mathlib.Tactic.Ring.mul_pf_left {R : Type u_1} [inst : CommSemiring R] {a₃ : R} {b : R} {c : R} (a₁ : R) (a₂ : ℕ) : a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

ink

theorem Mathlib.Tactic.Ring.mul_pf_right {R : Type u_1} [inst : CommSemiring R] {a : R} {b₃ : R} {c : R} (b₁ : R) (b₂ : ℕ) : a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

ink

theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap {R : Type u_1} [inst : CommSemiring R] {ea : ℕ} {eb : ℕ} {e : ℕ} {a₂ : R} {b₂ : R} {c : R} (x : R) : ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

ink

partial def Mathlib.Tactic.Ring.evalMulProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExProd sα a) (vb : Mathlib.Tactic.Ring.ExProd sα b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

Multiplies two monomials va, vb together to get a normalized result monomial.

• x * y = (x * y) (for x, y coefficients)
• x * (b₁ * b₂) = b₁ * (b₂ * x) (for x coefficient)
• (a₁ * a₂) * y = a₁ * (a₂ * y) (for y coefficient)
• (x ^ ea * a₂) * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂) (if ea and eb are identical except coefficient)
• (a₁ * a₂) * (b₁ * b₂) = a₁ * (a₂ * (b₁ * b₂)) (if a₁.lt b₁)
• (a₁ * a₂) * (b₁ * b₂) = b₁ * ((a₁ * a₂) * b₂) (if not a₁.lt b₁)

ink

theorem Mathlib.Tactic.Ring.mul_zero {R : Type u_1} [inst : CommSemiring R] (a : R) : a * 0 = 0

ink

theorem Mathlib.Tactic.Ring.mul_add {R : Type u_1} [inst : CommSemiring R] {a : R} {b₁ : R} {c₁ : R} {b₂ : R} {c₂ : R} {d : R} : a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d

ink

def Mathlib.Tactic.Ring.evalMul₁ {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExProd sα a) (vb : Mathlib.Tactic.Ring.ExSum sα b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

Multiplies a monomial va to a polynomial vb to get a normalized result polynomial.

• a * 0 = 0
• a * (b₁ + b₂) = (a * b₁) + (a * b₂)

Equations

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

ink

theorem Mathlib.Tactic.Ring.zero_mul {R : Type u_1} [inst : CommSemiring R] (b : R) : 0 * b = 0

ink

theorem Mathlib.Tactic.Ring.add_mul {R : Type u_1} [inst : CommSemiring R] {a₁ : R} {b : R} {c₁ : R} {a₂ : R} {c₂ : R} {d : R} : a₁ * b = c₁ → a₂ * b = c₂ → c₁ + c₂ = d → (a₁ + a₂) * b = d

ink

def Mathlib.Tactic.Ring.evalMul {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum sα a) (vb : Mathlib.Tactic.Ring.ExSum sα b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonUnitalNonAssocSemiring.toMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toNonUnitalNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

Multiplies two polynomials va, vb together to get a normalized result polynomial.

• 0 * b = 0
• (a₁ + a₂) * b = (a₁ * b) + (a₂ * b)

Equations

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

ink

theorem Mathlib.Tactic.Ring.natCast_nat {R : Type u_1} [inst : CommSemiring R] (n : ℕ) : ↑(Nat.rawCast n) = Nat.rawCast n

ink

theorem Mathlib.Tactic.Ring.natCast_mul {R : Type u_1} [inst : CommSemiring R] {a₁ : ℕ} {b₁ : R} {a₃ : ℕ} {b₃ : R} (a₂ : ℕ) : ↑a₁ = b₁ → ↑a₃ = b₃ → ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

ink

theorem Mathlib.Tactic.Ring.natCast_zero {R : Type u_1} [inst : CommSemiring R] : ↑0 = 0

ink

theorem Mathlib.Tactic.Ring.natCast_add {R : Type u_1} [inst : CommSemiring R] {a₁ : ℕ} {b₁ : R} {a₂ : ℕ} {b₂ : R} : ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

ink

partial def Mathlib.Tactic.Ring.ExBase.evalNatCast {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExBase Mathlib.Tactic.Ring.sℕ a) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExBase sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.cast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNatCast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))) a)))

Applies Nat.cast to a nat polynomial to produce a polynomial in α.

• An atom e causes ↑e↑e to be allocated as a new atom.
• A sum delegates to ExSum.evalNatCast.

ink

partial def Mathlib.Tactic.Ring.ExProd.evalNatCast {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ a) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.cast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNatCast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))) a)))

Applies Nat.cast to a nat monomial to produce a monomial in α.

• ↑c = c↑c = c if c is a numeric literal
• ↑(a ^ n * b) = ↑a ^ n * ↑b↑(a ^ n * b) = ↑a ^ n * ↑b↑a ^ n * ↑b↑b

ink

partial def Mathlib.Tactic.Ring.ExSum.evalNatCast {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExSum Mathlib.Tactic.Ring.sℕ a) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.cast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNatCast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))) a)))

Applies Nat.cast to a nat polynomial to produce a polynomial in α.

• ↑0 = 0↑0 = 0
• ↑(a + b) = ↑a + ↑b↑(a + b) = ↑a + ↑b↑a + ↑b↑b

ink

theorem Mathlib.Tactic.Ring.smul_nat {a : ℕ} {b : ℕ} {c : ℕ} : a * b = c → a • b = c

ink

theorem Mathlib.Tactic.Ring.smul_eq_cast {R : Type u_1} [inst : CommSemiring R] {a : ℕ} {a' : R} {b : R} {c : R} : ↑a = a' → a' * b = c → a • b = c

ink

def Mathlib.Tactic.Ring.evalNSMul {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Q(ℕ)} {b : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum Mathlib.Tactic.Ring.sℕ a) (vb : Mathlib.Tactic.Ring.ExSum sα b) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HSMul.hSMul [Lean.Level.zero, u, u]) (Lean.Expr.const `Nat [])) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHSMul [Lean.Level.zero, u]) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddMonoid.SMul [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne.toAddMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddCommMonoidWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toAddCommMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))))) a) b)))

Constructs the scalar multiplication n • a, where both n : ℕ and a : α are normalized polynomial expressions.

• a • b = a * b if α = ℕ
• a • b = ↑a * b↑a * b otherwise

Equations

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

ink

theorem Mathlib.Tactic.Ring.neg_one_mul {R : Type u_1} [inst : Ring R] {a : R} {b : R} : Int.rawCast (Int.negOfNat 1) * a = b → -a = b

ink

theorem Mathlib.Tactic.Ring.neg_mul {R : Type u_1} [inst : Ring R] (a₁ : R) (a₂ : ℕ) {a₃ : R} {b : R} : -a₃ = b → -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

ink

def Mathlib.Tactic.Ring.evalNegProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) (va : Mathlib.Tactic.Ring.ExProd sα a) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Neg.neg [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toNeg [u]) α) rα)) a))

Negates a monomial va to get another monomial.

• -c = (-c) (for c coefficient)
• -(a₁ * a₂) = a₁ * -a₂

ink

theorem Mathlib.Tactic.Ring.neg_zero {R : Type u_1} [inst : Ring R] : -0 = 0

ink

theorem Mathlib.Tactic.Ring.neg_add {R : Type u_1} [inst : Ring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} : -a₁ = b₁ → -a₂ = b₂ → -(a₁ + a₂) = b₁ + b₂

ink

def Mathlib.Tactic.Ring.evalNeg {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) (va : Mathlib.Tactic.Ring.ExSum sα a) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Neg.neg [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toNeg [u]) α) rα)) a))

Negates a polynomial va to get another polynomial.

• -0 = 0 (for c coefficient)
• -(a₁ + a₂) = -a₁ + -a₂

Equations

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

ink

theorem Mathlib.Tactic.Ring.sub_pf {R : Type u_1} [inst : Ring R] {a : R} {b : R} {c : R} {d : R} : -b = c → a + c = d → a - b = d

ink

def Mathlib.Tactic.Ring.evalSub {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) (va : Mathlib.Tactic.Ring.ExSum sα a) (vb : Mathlib.Tactic.Ring.ExSum sα b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HSub.hSub [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHSub [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toSub [u]) α) rα))) a) b))

Subtracts two polynomials va, vb to get a normalized result polynomial.

• a - b = a + -b

Equations

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

ink

theorem Mathlib.Tactic.Ring.pow_prod_atom {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ℕ) : a ^ b = (a + 0) ^ b * Nat.rawCast 1

ink

def Mathlib.Tactic.Ring.evalPowProdAtom {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExProd sα a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

The fallback case for exponentiating polynomials is to use ExBase.toProd to just build an exponent expression. (This has a slightly different normalization than evalPowAtom because the input types are different.)

• x ^ e = (x + 0) ^ e * 1

Equations

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

ink

theorem Mathlib.Tactic.Ring.pow_atom {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ℕ) : a ^ b = a ^ b * Nat.rawCast 1 + 0

ink

def Mathlib.Tactic.Ring.evalPowAtom {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExBase sα a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

The fallback case for exponentiating polynomials is to use ExBase.toProd to just build an exponent expression.

• x ^ e = x ^ e * 1 + 0

Equations

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

ink

theorem Mathlib.Tactic.Ring.const_pos (n : ℕ) (h : Nat.ble 1 n = true) : 0 < Nat.rawCast n

ink

theorem Mathlib.Tactic.Ring.mul_exp_pos {a₁ : ℕ} {a₂ : ℕ} (n : ℕ) (h₁ : 0 < a₁) (h₂ : 0 < a₂) : 0 < a₁ ^ n * a₂

ink

theorem Mathlib.Tactic.Ring.add_pos_left {a₁ : ℕ} (a₂ : ℕ) (h : 0 < a₁) : 0 < a₁ + a₂

ink

theorem Mathlib.Tactic.Ring.add_pos_right {a₂ : ℕ} (a₁ : ℕ) (h : 0 < a₂) : 0 < a₁ + a₂

ink

partial def Mathlib.Tactic.Ring.ExBase.evalPos {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExBase Mathlib.Tactic.Ring.sℕ a) : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `LT.lt [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.const `instLTNat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.lit (Lean.Literal.natVal 0))) (Lean.Expr.app (Lean.Expr.const `instOfNatNat []) (Lean.Expr.lit (Lean.Literal.natVal 0))))) a))

Attempts to prove that a polynomial expression in ℕ is positive.

• Atoms are not (necessarily) positive
• Sums defer to ExSum.evalPos

ink

partial def Mathlib.Tactic.Ring.ExProd.evalPos {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ a) : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `LT.lt [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.const `instLTNat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.lit (Lean.Literal.natVal 0))) (Lean.Expr.app (Lean.Expr.const `instOfNatNat []) (Lean.Expr.lit (Lean.Literal.natVal 0))))) a))

Attempts to prove that a monomial expression in ℕ is positive.

• 0 < c (where c is a numeral) is true by the normalization invariant (c is not zero)
• 0 < x ^ e * b if 0 < x and 0 < b

ink

partial def Mathlib.Tactic.Ring.ExSum.evalPos {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExSum Mathlib.Tactic.Ring.sℕ a) : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `LT.lt [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.const `instLTNat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.lit (Lean.Literal.natVal 0))) (Lean.Expr.app (Lean.Expr.const `instOfNatNat []) (Lean.Expr.lit (Lean.Literal.natVal 0))))) a))

Attempts to prove that a polynomial expression in ℕ is positive.

• 0 < 0 fails
• 0 < a + b if 0 < a or 0 < b

ink

theorem Mathlib.Tactic.Ring.pow_one {R : Type u_1} [inst : CommSemiring R] (a : R) : a ^ 1 = a

ink

theorem Mathlib.Tactic.Ring.pow_bit0 {R : Type u_1} [inst : CommSemiring R] {a : R} {k : ℕ} {b : R} {c : R} : a ^ k = b → b * b = c → a ^ Nat.mul 2 k = c

ink

theorem Mathlib.Tactic.Ring.pow_bit1 {R : Type u_1} [inst : CommSemiring R] {a : R} {k : ℕ} {b : R} {c : R} {d : R} : a ^ k = b → b * b = c → c * a = d → a ^ Nat.add (Nat.mul 2 k) 1 = d

ink

partial def Mathlib.Tactic.Ring.evalPowNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} (va : Mathlib.Tactic.Ring.ExSum sα a) (n : Q(ℕ)) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) n))

The main case of exponentiation of ring expressions is when va is a polynomial and n is a nonzero literal expression, like (x + y)^5. In this case we work out the polynomial completely into a sum of monomials.

• x ^ 1 = x
• x ^ (2*n) = x ^ n * x ^ n
• x ^ (2*n+1) = x ^ n * x ^ n * x

ink

theorem Mathlib.Tactic.Ring.one_pow {R : Type u_1} [inst : CommSemiring R] (b : ℕ) : Nat.rawCast 1 ^ b = Nat.rawCast 1

ink

theorem Mathlib.Tactic.Ring.mul_pow {R : Type u_1} [inst : CommSemiring R] {ea₁ : ℕ} {b : ℕ} {c₁ : ℕ} {a₂ : R} {c₂ : R} {xa₁ : R} : ea₁ * b = c₁ → a₂ ^ b = c₂ → (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

ink

def Mathlib.Tactic.Ring.evalPowProd {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExProd sα a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

There are several special cases when exponentiating monomials:

• 1 ^ n = 1
• x ^ y = (x ^ y) when x and y are constants
• (a * b) ^ e = a ^ e * b ^ e

In all other cases we use evalPowProdAtom.

ink

structure Mathlib.Tactic.Ring.ExtractCoeff (e : Q(ℕ)) : Type

• A raw natural number literal.

  k : Q(ℕ)

• The result of extracting the coefficient is a monic monomial.

  e' : Q(ℕ)

• e' is a monomial.

  ve' : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ e'

• The proof that e splits into the coefficient k and the monic monomial e'.

  p : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Eq [Lean.Level.succ Lean.Level.zero]) (Lean.Expr.const `Nat [])) e) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HMul.hMul [Lean.Level.zero, Lean.Level.zero, Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.const `Nat [])) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHMul [Lean.Level.zero]) (Lean.Expr.const `Nat [])) (Lean.Expr.const `instMulNat []))) e') k))

The result of extractCoeff is a numeral and a proof that the original expression factors by this numeral.

ink

theorem Mathlib.Tactic.Ring.coeff_one (k : ℕ) : Nat.rawCast k = Nat.rawCast 1 * k

ink

theorem Mathlib.Tactic.Ring.coeff_mul {a₃ : ℕ} {c₂ : ℕ} {k : ℕ} (a₁ : ℕ) (a₂ : ℕ) : a₃ = c₂ * k → a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

ink

def Mathlib.Tactic.Ring.extractCoeff {a : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ a) : Mathlib.Tactic.Ring.ExtractCoeff a

Given a monomial expression va, splits off the leading coefficient k and the remainder e', stored in the ExtractCoeff structure.

• c = 1 * c (if c is a constant)
• a * b = (a * b') * k if b = b' * k

ink

theorem Mathlib.Tactic.Ring.pow_one_cast {R : Type u_1} [inst : CommSemiring R] (a : R) : a ^ Nat.rawCast 1 = a

ink

theorem Mathlib.Tactic.Ring.zero_pow {R : Type u_1} [inst : CommSemiring R] {b : ℕ} : 0 < b → 0 ^ b = 0

ink

theorem Mathlib.Tactic.Ring.single_pow {R : Type u_1} [inst : CommSemiring R] {a : R} {b : ℕ} {c : R} : a ^ b = c → (a + 0) ^ b = c + 0

ink

theorem Mathlib.Tactic.Ring.pow_nat {R : Type u_1} [inst : CommSemiring R] {b : ℕ} {c : ℕ} {k : ℕ} {a : R} {d : R} {e : R} : b = c * k → a ^ c = d → d ^ k = e → a ^ b = e

ink

partial def Mathlib.Tactic.Ring.evalPow₁ {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExSum sα a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

Exponentiates a polynomial va by a monomial vb, including several special cases.

• a ^ 1 = a
• 0 ^ e = 0 if 0 < e
• (a + 0) ^ b = a ^ b computed using evalPowProd
• a ^ b = (a ^ b') ^ k if b = b' * k and k > 1

Otherwise a ^ b is just encoded as a ^ b * 1 + 0 using evalPowAtom.

ink

theorem Mathlib.Tactic.Ring.pow_zero {R : Type u_1} [inst : CommSemiring R] (a : R) : a ^ 0 = Nat.rawCast 1 + 0

ink

theorem Mathlib.Tactic.Ring.pow_add {R : Type u_1} [inst : CommSemiring R] {a : R} {b₁ : ℕ} {c₁ : R} {b₂ : ℕ} {c₂ : R} {d : R} : a ^ b₁ = c₁ → a ^ b₂ = c₂ → c₁ * c₂ = d → a ^ (b₁ + b₂) = d

ink

def Mathlib.Tactic.Ring.evalPow {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Q(ℕ)} (va : Mathlib.Tactic.Ring.ExSum sα a) (vb : Mathlib.Tactic.Ring.ExSum Mathlib.Tactic.Ring.sℕ b) : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HPow.hPow [u, Lean.Level.zero, u]) α) (Lean.Expr.const `Nat [])) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHPow [u, Lean.Level.zero]) α) (Lean.Expr.const `Nat [])) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Monoid.Pow [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `MonoidWithZero.toMonoid [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toMonoidWithZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα)))))) a) b))

Exponentiates two polynomials va, vb.

• a ^ 0 = 1
• a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂

Equations

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

ink

structure Mathlib.Tactic.Ring.Cache {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) : Type

• A ring instance on α, if available.

  rα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α))

• A division ring instance on α, if available.

  dα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α))

• A characteristic zero ring instance on α, if available.

  czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddCommMonoidWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `NonAssocSemiring.toAddCommMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Semiring.toNonAssocSemiring [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CommSemiring.toSemiring [u]) α) sα))))))

This cache contains data required by the ring tactic during execution.

ink

def Mathlib.Tactic.Ring.mkCache {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) : Lean.MetaM (Mathlib.Tactic.Ring.Cache sα)

Create a new cache for α by doing the necessary instance searches.

Equations

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

ink

theorem Mathlib.Tactic.Ring.cast_pos {R : Type u_1} [inst : CommSemiring R] {a : R} {n : ℕ} : Mathlib.Meta.NormNum.IsNat a n → a = Nat.rawCast n + 0

ink

theorem Mathlib.Tactic.Ring.cast_zero {R : Type u_1} [inst : CommSemiring R] {a : R} : Mathlib.Meta.NormNum.IsNat a 0 → a = 0

ink

theorem Mathlib.Tactic.Ring.cast_neg {n : ℕ} {R : Type u_1} [inst : Ring R] {a : R} : Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → a = Int.rawCast (Int.negOfNat n) + 0

ink

theorem Mathlib.Tactic.Ring.cast_rat {n : ℤ} {d : ℕ} {R : Type u_1} [inst : DivisionRing R] {a : R} : Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d + 0

ink

def Mathlib.Tactic.Ring.evalCast {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {e : Qq.QQ α} : Mathlib.Meta.NormNum.Result e → Option (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) e)

Converts a proof by norm_num that e is a numeral, into a normalization as a monomial:

• e = 0 if norm_num returns IsNat e 0
• e = Nat.rawCast n + 0 if norm_num returns IsNat e n
• e = Int.rawCast n + 0 if norm_num returns IsInt e n
• e = Rat.rawCast n d + 0 if norm_num returns IsRat e n d

Equations

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

ink

theorem Mathlib.Tactic.Ring.toProd_pf {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} (p : a = a') : a = a' ^ Nat.rawCast 1 * Nat.rawCast 1

ink

theorem Mathlib.Tactic.Ring.atom_pf {R : Type u_1} [inst : CommSemiring R] (a : R) : a = a ^ Nat.rawCast 1 * Nat.rawCast 1 + 0

ink

theorem Mathlib.Tactic.Ring.atom_pf' {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} (p : a = a') : a = a' ^ Nat.rawCast 1 * Nat.rawCast 1 + 0

ink

def Mathlib.Tactic.Ring.evalAtom {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (e : Qq.QQ α) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) e)

Evaluates an atom, an expression where ring can find no additional structure.

• a = a ^ 1 * 1 + 0

Equations

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

ink

theorem Mathlib.Tactic.Ring.inv_mul {R : Type u_1} [inst : DivisionRing R] {a₁ : R} {a₂ : ℕ} {a₃ : R} {b₁ : R} {b₃ : R} {c : R} : a₁⁻¹ = b₁ → a₃⁻¹ = b₃ → b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c → (a₁ ^ a₂ * a₃)⁻¹ = c

ink

theorem Mathlib.Tactic.Ring.inv_zero {R : Type u_1} [inst : DivisionRing R] : 0⁻¹ = 0

ink

theorem Mathlib.Tactic.Ring.inv_single {R : Type u_1} [inst : DivisionRing R] {a : R} {b : R} : a⁻¹ = b → (a + 0)⁻¹ = b + 0

ink

theorem Mathlib.Tactic.Ring.inv_add {R : Type u_1} [inst : CommSemiring R] {a₁ : ℕ} {b₁ : R} {a₂ : ℕ} {b₂ : R} : ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

ink

def Mathlib.Tactic.Ring.evalInvAtom {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (dα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) (a : Qq.QQ α) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExBase sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Inv.inv [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toInv [u]) α) dα)) a)))

Applies ⁻¹⁻¹ to a polynomial to get an atom.

Equations

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

ink

def Mathlib.Tactic.Ring.ExProd.evalInv {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (dα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) {a : Qq.QQ α} (czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) dα)))))) (va : Mathlib.Tactic.Ring.ExProd sα a) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Inv.inv [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toInv [u]) α) dα)) a)))

Inverts a polynomial va to get a normalized result polynomial.

• c⁻¹ = (c⁻¹)⁻¹ = (c⁻¹)⁻¹) if c is a constant
• (a ^ b * c)⁻¹ = a⁻¹ ^ b * c⁻¹⁻¹ = a⁻¹ ^ b * c⁻¹⁻¹ ^ b * c⁻¹⁻¹

ink

def Mathlib.Tactic.Ring.ExSum.evalInv {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (dα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) {a : Qq.QQ α} (czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) dα)))))) (va : Mathlib.Tactic.Ring.ExSum sα a) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Inv.inv [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toInv [u]) α) dα)) a)))

Inverts a polynomial va to get a normalized result polynomial.

• 0⁻¹ = 0⁻¹ = 0
• a⁻¹ = (a⁻¹)⁻¹ = (a⁻¹)⁻¹) if a is a nontrivial sum

Equations

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

ink

theorem Mathlib.Tactic.Ring.div_pf {R : Type u_1} [inst : DivisionRing R] {a : R} {b : R} {c : R} {d : R} : b⁻¹ = c → a * c = d → a / b = d

ink

def Mathlib.Tactic.Ring.evalDiv {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) {a : Qq.QQ α} {b : Qq.QQ α} (rα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) (czα : Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) rα)))))) (va : Mathlib.Tactic.Ring.ExSum sα a) (vb : Mathlib.Tactic.Ring.ExSum sα b) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) (Qq.QQ.qq (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `HDiv.hDiv [u, u, u]) α) α) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `instHDiv [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toDiv [u]) α) rα))) a) b)))

Divides two polynomials va, vb to get a normalized result polynomial.

• a / b = a * b⁻¹⁻¹

Equations

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

ink

theorem Mathlib.Tactic.Ring.add_congr {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' + b' = c → a + b = c

ink

theorem Mathlib.Tactic.Ring.mul_congr {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' * b' = c → a * b = c

ink

theorem Mathlib.Tactic.Ring.nsmul_congr {R : Type u_1} [inst : CommSemiring R] {a : ℕ} {a' : ℕ} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' • b' = c → a • b = c

ink

theorem Mathlib.Tactic.Ring.pow_congr {R : Type u_1} [inst : CommSemiring R] {a : R} {a' : R} {b : ℕ} {b' : ℕ} {c : R} : a = a' → b = b' → a' ^ b' = c → a ^ b = c

ink

theorem Mathlib.Tactic.Ring.neg_congr {R : Type u_1} [inst : Ring R] {a : R} {a' : R} {b : R} : a = a' → -a' = b → -a = b

ink

theorem Mathlib.Tactic.Ring.sub_congr {R : Type u_1} [inst : Ring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' - b' = c → a - b = c

ink

theorem Mathlib.Tactic.Ring.inv_congr {R : Type u_1} [inst : DivisionRing R] {a : R} {a' : R} {b : R} : a = a' → a'⁻¹ = b → a⁻¹ = b

ink

theorem Mathlib.Tactic.Ring.div_congr {R : Type u_1} [inst : DivisionRing R] {a : R} {a' : R} {b : R} {b' : R} {c : R} : a = a' → b = b' → a' / b' = c → a / b = c

ink

def Mathlib.Tactic.Ring.Cache.nat : Mathlib.Tactic.Ring.Cache Mathlib.Tactic.Ring.sℕ

A precomputed Cache for ℕ.

Equations

• Mathlib.Tactic.Ring.Cache.nat = { rα := none, dα := none, czα := some q((_ : CharZero ℕ)) }

ink

def Mathlib.Tactic.Ring.isAtomOrDerivable {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (c : Mathlib.Tactic.Ring.Cache sα) (e : Qq.QQ α) : Mathlib.Tactic.AtomM (Option (Option (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) e)))

Checks whether e would be processed by eval as a ring expression, or otherwise if it is an atom or something simplifiable via norm_num.

We use this in ring_ng to avoid rewriting atoms unnecessarily.

Returns:

• none if eval would process e as an algebraic ring expression
• some none if eval would treat e as an atom.
• some (some r) if eval would not process e as an algebraic ring expression, but NormNum.derive can nevertheless simplify e, with result r.

Equations

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

ink

partial def Mathlib.Tactic.Ring.eval {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `CommSemiring [u]) α)) (c : Mathlib.Tactic.Ring.Cache sα) (e : Qq.QQ α) : Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) e)

Evaluates expression e of type α into a normalized representation as a polynomial. This is the main driver of ring, which calls out to evalAdd, evalMul etc.

ink

theorem Mathlib.Tactic.Ring.of_eq {R : Type u_1} {a : R} {c : R} {b : R} : a = c → b = c → a = b

ink

opaque Mathlib.Tactic.Ring.ringCleanupRef : IO.Ref (Lean.Expr → Lean.MetaM Lean.Expr)

This is a routine which is used to clean up the unsolved subgoal of a failed ring1 application. It is overridden in Mathlib.Tactic.Ring.RingNF to apply the ring_nf simp set to the goal.

ink

def Mathlib.Tactic.Ring.proveEq (g : Lean.MVarId) : Mathlib.Tactic.AtomM Unit

Frontend of ring1: attempt to close a goal g, assuming it is an equation of semirings.

Equations

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

ink

def Mathlib.Tactic.Ring.ring1 : Lean.ParserDescr

Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

• This version of ring fails if the target is not an equality.
• The variant ring1! will use a more aggressive reducibility setting to determine equality of atoms.

Equations

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

ink

def Mathlib.Tactic.Ring.tacticRing1! : Lean.ParserDescr

Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

• This version of ring fails if the target is not an equality.
• The variant ring1! will use a more aggressive reducibility setting to determine equality of atoms.

Equations

• Mathlib.Tactic.Ring.tacticRing1! = Lean.ParserDescr.node `Mathlib.Tactic.Ring.tacticRing1! 1024 (Lean.ParserDescr.nonReservedSymbol "ring1!" false)