theorem Hex.DensePoly.neg_neg_poly {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (p : DensePoly R) : - -p = p

Dense-polynomial negation is involutive.

@[irreducible]

def Hex.DensePoly.natPow {R : Type u} [Zero R] [One R] [Add R] [Mul R] [DecidableEq R] (p : DensePoly R) (n : Nat) : DensePoly R

Natural powers by binary exponentiation.

Equations

• p.natPow n = if n = 0 then 1 else if n = 1 then p else have square := (p * p).natPow (n / 2); if n % 2 = 0 then square else square * p

@[simp]

theorem Hex.DensePoly.natPow_one {R : Type u} [Zero R] [One R] [Add R] [Mul R] [DecidableEq R] (p : DensePoly R) : p.natPow 1 = p

Exponent one returns the input without polynomial multiplication.

@[simp]

theorem Hex.DensePoly.natPow_two {R : Type u} [Zero R] [One R] [Add R] [Mul R] [DecidableEq R] (p : DensePoly R) : p.natPow 2 = p * p

Exponent two performs just the required polynomial square.

@[simp]

theorem Hex.DensePoly.natPow_zero {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (p : DensePoly R) : p.natPow 0 = 1

theorem Hex.DensePoly.natPow_succ {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (p : DensePoly R) (n : Nat) : p.natPow (n + 1) = p.natPow n * p

@[instance_reducible]

instance Hex.DensePoly.instNatCast {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : NatCast (DensePoly R)

Natural-number casts are constant polynomials, reusing zero and one.

Equations

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

@[instance_reducible]

instance Hex.DensePoly.instOfNat {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (n : Nat) : OfNat (DensePoly R) n

Numerals are constant polynomials, reusing zero and one.

Equations

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

@[instance_reducible]

instance Hex.DensePoly.instNSMul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : SMul Nat (DensePoly R)

Natural scalar multiplication is multiplication by the cast constant.

Equations

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

@[instance_reducible]

instance Hex.DensePoly.instNPow {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : HPow (DensePoly R) Nat (DensePoly R)

Natural powers of dense polynomials.

Equations

• Hex.DensePoly.instNPow = { hPow := Hex.DensePoly.natPow }

@[instance_reducible]

instance Hex.DensePoly.instIntCast {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : IntCast (DensePoly R)

Integer casts are signed constant polynomials.

Equations

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

@[instance_reducible]

instance Hex.DensePoly.instZSMul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : SMul Int (DensePoly R)

Integer scalar multiplication is signed natural scalar multiplication.

Equations

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

@[simp]

theorem Hex.DensePoly.coeff_ofNat {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (n i : Nat) : coeff (OfNat.ofNat n) i = if i = 0 then OfNat.ofNat n else 0

A numeral polynomial stores its value in coefficient zero only.

@[simp]

theorem Hex.DensePoly.coeff_natCast {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (n i : Nat) : (↑n).coeff i = if i = 0 then ↑n else 0

A cast-natural polynomial stores its value in coefficient zero only.

@[instance_reducible]

instance Hex.instGrindSemiringDensePoly {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : Lean.Grind.Semiring (DensePoly R)

Dense 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.instGrindRingDensePoly {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : Lean.Grind.Ring (DensePoly R)

Dense 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.instGrindCommRingDensePoly {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : Lean.Grind.CommRing (DensePoly R)

Dense polynomial multiplication is commutative when coefficient multiplication is.

Equations

• Hex.instGrindCommRingDensePoly = { toRing := Hex.instGrindRingDensePoly, mul_comm := ⋯ }