@[instance_reducible]

instance Hex.MvPoly.instNatCast {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : NatCast (MvPoly n R cmp)

Natural number numerals, as constant polynomials.

Equations

• Hex.MvPoly.instNatCast = { natCast := fun (k : Nat) => match k with | 0 => Zero.zero | 1 => One.one | k.succ.succ => Hex.MvPoly.C ↑(k + 2) }

@[instance_reducible]

instance Hex.MvPoly.instOfNat {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (k : Nat) : OfNat (MvPoly n R cmp) k

Equations

• Hex.MvPoly.instOfNat 0 = { ofNat := Zero.zero }
• Hex.MvPoly.instOfNat 1 = { ofNat := One.one }
• Hex.MvPoly.instOfNat k_2.succ.succ = { ofNat := Hex.MvPoly.C (OfNat.ofNat (k_2 + 2)) }

@[instance_reducible]

instance Hex.MvPoly.instNSMul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : SMul Nat (MvPoly n R cmp)

Equations

• Hex.MvPoly.instNSMul = { smul := fun (k : Nat) (p : Hex.MvPoly n R cmp) => ↑k * p }

@[instance_reducible]

instance Hex.MvPoly.instIntCast {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : IntCast (MvPoly n R cmp)

Equations

• Hex.MvPoly.instIntCast = { intCast := fun (i : Int) => match i with | Int.ofNat k => ↑k | Int.negSucc k => -↑(k + 1) }

@[instance_reducible]

instance Hex.MvPoly.instZSMul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : SMul Int (MvPoly n R cmp)

Equations

• Hex.MvPoly.instZSMul = { smul := fun (i : Int) (p : Hex.MvPoly n R cmp) => match i with | Int.ofNat k => k • p | Int.negSucc k => -((k + 1) • p) }

@[simp]

theorem Hex.MvPoly.coeff_ofNat {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (k : Nat) (m : Mono n) : coeff m (OfNat.ofNat k) = if m = Mono.zero then OfNat.ofNat k else 0

Numerals are constant polynomials.

@[simp]

theorem Hex.MvPoly.coeff_natCast {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (k : Nat) (m : Mono n) : coeff m ↑k = if m = Mono.zero then ↑k else 0

The canonical map from the natural numbers lands in the constants.

theorem Hex.MvPoly.pow_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (p : MvPoly n R cmp) : p ^ 0 = 1

The zeroth power is one.

npowBySq is defined by well-founded recursion, so it is @[irreducible] and rfl does not see through it; the equation lemma does.

@[simp]

theorem Hex.MvPoly.neg_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : -0 = 0

Negating zero gives zero.

@[simp]

theorem Hex.MvPoly.neg_neg {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (p : MvPoly n R cmp) : - -p = p

Negation is an involution.

theorem Hex.MvPoly.neg_add_cancel {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (p : MvPoly n R cmp) : -p + p = 0

Negation is the left inverse of addition.

theorem Hex.MvPoly.sub_eq_add_neg {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (p q : MvPoly n R cmp) : p - q = p + -q

Subtraction is addition of the negation.

theorem Hex.MvPoly.nsmul_eq_natCast_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (k : Nat) (p : MvPoly n R cmp) : k • p = ↑k * p

Multiplying by a natural numeral is scalar multiplication.

theorem Hex.MvPoly.ofNat_succ {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (k : Nat) : OfNat.ofNat (k + 1) = OfNat.ofNat k + 1

Successor numerals add one.

theorem Hex.MvPoly.ofNat_eq_natCast {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] (k : Nat) : OfNat.ofNat k = ↑k

Numerals agree with the canonical map from the natural numbers.

@[instance_reducible]

instance Hex.MvPoly.instGrindSemiring {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : Lean.Grind.Semiring (MvPoly n R cmp)

Multivariate polynomials over a lightweight commutative ring form a lightweight semiring.

Equations

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

@[instance_reducible]

instance Hex.MvPoly.instGrindRing {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : Lean.Grind.Ring (MvPoly n R cmp)

Multivariate polynomials over a lightweight commutative ring form a lightweight ring.

Equations

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

@[instance_reducible]

instance Hex.MvPoly.instGrindCommRing {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommRing R] [DecidableEq R] : Lean.Grind.CommRing (MvPoly n R cmp)

Multivariate polynomial multiplication is commutative when coefficient multiplication is.

Equations

• Hex.MvPoly.instGrindCommRing = { toRing := Hex.MvPoly.instGrindRing, mul_comm := ⋯ }