noncomputable def HexMvPolyMathlib.monoEquiv {n : ℕ} : Hex.Mono n ≃ (Fin n →₀ ℕ)

A fixed-arity exponent vector is equivalent to a finitely supported function on the finite variable type.

Equations

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

@[simp]

theorem HexMvPolyMathlib.monoEquiv_apply {n : ℕ} (m : Hex.Mono n) (i : Fin n) : (monoEquiv m) i = m[i]

The finitely supported image of a monomial has the same exponent at every variable.

@[simp]

theorem HexMvPolyMathlib.monoEquiv_symm_apply {n : ℕ} (d : Fin n →₀ ℕ) (i : Fin n) : Vector.get (monoEquiv.symm d) i = d i

Converting a finitely supported exponent function back to a monomial preserves every exponent.

@[simp]

theorem HexMvPolyMathlib.monoEquiv_zero {n : ℕ} : monoEquiv Hex.Mono.zero = 0

The zero monomial corresponds to the zero finitely supported function.

@[simp]

theorem HexMvPolyMathlib.monoEquiv_eq_zero {n : ℕ} (m : Hex.Mono n) : monoEquiv m = 0 ↔ m = Hex.Mono.zero

A monomial maps to zero exactly when it is the zero monomial.

@[simp]

theorem HexMvPolyMathlib.zero_eq_monoEquiv {n : ℕ} (m : Hex.Mono n) : 0 = monoEquiv m ↔ m = Hex.Mono.zero

Zero equals a mapped monomial exactly when that monomial is zero.

@[simp]

theorem HexMvPolyMathlib.monoEquiv_mul {n : ℕ} (a b : Hex.Mono n) : monoEquiv (a.mul b) = monoEquiv a + monoEquiv b

Monomial multiplication corresponds to addition of finitely supported exponent functions.

@[simp]

theorem HexMvPolyMathlib.monoEquiv_unit {n : ℕ} (i : Fin n) : monoEquiv (Hex.Mono.unit i) = Finsupp.single i 1

A unit monomial corresponds to Mathlib's single-variable exponent.

noncomputable def HexMvPolyMathlib.monoPairEquiv {n : ℕ} : Hex.Mono n × Hex.Mono n ≃ (Fin n →₀ ℕ) × (Fin n →₀ ℕ)

The componentwise exponent equivalence on pairs of monomials.

Equations

• HexMvPolyMathlib.monoPairEquiv = HexMvPolyMathlib.monoEquiv.prodCongr HexMvPolyMathlib.monoEquiv

@[simp]

theorem HexMvPolyMathlib.monoPairEquiv_apply {n : ℕ} (ab : Hex.Mono n × Hex.Mono n) : monoPairEquiv ab = (monoEquiv ab.1, monoEquiv ab.2)

The pair equivalence maps both monomials componentwise.

@[simp]

theorem HexMvPolyMathlib.monoPairEmbedding_apply {n : ℕ} (ab : Hex.Mono n × Hex.Mono n) : monoPairEquiv.toEmbedding ab = (monoEquiv ab.1, monoEquiv ab.2)

The pair embedding applies the monomial equivalence to each component.

noncomputable def HexMvPolyMathlib.toMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : MvPolynomial (Fin n) R

Interpret an executable sparse polynomial as a Mathlib multivariate polynomial by summing its canonical support.

Equations

• HexMvPolyMathlib.toMvPolynomial p = ∑ m ∈ p.monomials.toFinset, (MvPolynomial.monomial (HexMvPolyMathlib.monoEquiv m)) (Hex.MvPoly.coeff m p)

theorem HexMvPolyMathlib.toMvPolynomial_eq_sum {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : toMvPolynomial p = ∑ m ∈ p.monomials.toFinset, (MvPolynomial.monomial (monoEquiv m)) (Hex.MvPoly.coeff m p)

The canonical-support sum used by the forward conversion.

@[simp]

theorem HexMvPolyMathlib.coeff_toMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (m : Hex.Mono n) (p : Hex.MvPoly n R cmp) : MvPolynomial.coeff (monoEquiv m) (toMvPolynomial p) = Hex.MvPoly.coeff m p

Forward conversion preserves every coefficient.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_monomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (m : Hex.Mono n) (c : R) : toMvPolynomial (Hex.MvPoly.monomial m c) = (MvPolynomial.monomial (monoEquiv m)) c

Forward conversion preserves a single executable monomial.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_addMonomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) (m : Hex.Mono n) (c : R) : toMvPolynomial (p.addMonomial m c) = toMvPolynomial p + (MvPolynomial.monomial (monoEquiv m)) c

Adding one executable term is addition by the corresponding Mathlib monomial, including coefficient cancellation.

theorem HexMvPolyMathlib.toMvPolynomial_ofTerms {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (terms : List (Hex.Mono n × R)) : toMvPolynomial (Hex.MvPoly.ofTerms terms) = List.foldl (fun (p : MvPolynomial (Fin n) R) (term : Hex.Mono n × R) => p + (MvPolynomial.monomial (monoEquiv term.1)) term.2) 0 terms

Constructing from a term stream agrees with folding the corresponding Mathlib monomials. Duplicate monomials sum and cancellations disappear on both sides.

noncomputable def HexMvPolyMathlib.ofMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : MvPolynomial (Fin n) R) : Hex.MvPoly n R cmp

Rebuild an executable sparse polynomial from a Mathlib multivariate polynomial's finite support.

Equations

• HexMvPolyMathlib.ofMvPolynomial p = Hex.MvPoly.ofTerms (List.map (fun (d : Fin n →₀ ℕ) => (HexMvPolyMathlib.monoEquiv.symm d, MvPolynomial.coeff d p)) p.support.toList)

@[simp]

theorem HexMvPolyMathlib.coeff_ofMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (m : Hex.Mono n) (p : MvPolynomial (Fin n) R) : Hex.MvPoly.coeff m (ofMvPolynomial p) = MvPolynomial.coeff (monoEquiv m) p

Backward conversion preserves every coefficient.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_ofMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : MvPolynomial (Fin n) R) : toMvPolynomial (ofMvPolynomial p) = p

Converting a Mathlib polynomial to the executable representation and back recovers the original polynomial.

@[simp]

theorem HexMvPolyMathlib.ofMvPolynomial_toMvPolynomial {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : ofMvPolynomial (toMvPolynomial p) = p

Converting an executable polynomial to Mathlib and back recovers the canonical executable polynomial.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_zero {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] : toMvPolynomial 0 = 0

Forward conversion sends the executable zero to Mathlib zero.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_add {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p q : Hex.MvPoly n R cmp) : toMvPolynomial (p + q) = toMvPolynomial p + toMvPolynomial q

Forward conversion preserves addition.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_C {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (c : R) : toMvPolynomial (Hex.MvPoly.C c) = MvPolynomial.C c

Forward conversion sends executable constants to Mathlib constants.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_X {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (i : Fin n) : toMvPolynomial (Hex.MvPoly.X i) = MvPolynomial.X i

Forward conversion sends executable variables to Mathlib variables.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_one {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] : toMvPolynomial 1 = 1

Forward conversion preserves the multiplicative identity.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_mul {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p q : Hex.MvPoly n R cmp) : toMvPolynomial (p * q) = toMvPolynomial p * toMvPolynomial q

Forward conversion preserves multiplication.

theorem HexMvPolyMathlib.toMvPolynomial_injective {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] : Function.Injective toMvPolynomial

Forward conversion is injective.

theorem HexMvPolyMathlib.toMvPolynomial_surjective {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] : Function.Surjective toMvPolynomial

Forward conversion is surjective.

noncomputable def HexMvPolyMathlib.equiv {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] : Hex.MvPoly n R cmp ≃+* MvPolynomial (Fin n) R

The executable sparse representation is ring-equivalent to Mathlib's multivariate polynomials.

Equations

• HexMvPolyMathlib.equiv = { toFun := HexMvPolyMathlib.toMvPolynomial, invFun := HexMvPolyMathlib.ofMvPolynomial, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexMvPolyMathlib.equiv_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : equiv p = toMvPolynomial p

The ring equivalence applies as toMvPolynomial.

@[simp]

theorem HexMvPolyMathlib.equiv_symm_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : MvPolynomial (Fin n) R) : equiv.symm p = ofMvPolynomial p

The inverse ring equivalence applies as ofMvPolynomial.

@[implicit_reducible]

instance HexMvPolyMathlib.instNatCastMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] : NatCast (Hex.MvPoly n R cmp)

Natural casts are executable constant polynomials.

Equations

• HexMvPolyMathlib.instNatCastMvPoly = { natCast := fun (k : ℕ) => Hex.MvPoly.C ↑k }

@[implicit_reducible]

instance HexMvPolyMathlib.instSMulNatMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] : SMul ℕ (Hex.MvPoly n R cmp)

Natural scalar multiplication uses one executable constant product.

Equations

• HexMvPolyMathlib.instSMulNatMvPoly = { smul := fun (k : ℕ) (p : Hex.MvPoly n R cmp) => Hex.MvPoly.C ↑k * p }

theorem HexMvPolyMathlib.toMvPolynomial_nsmul {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (k : ℕ) (p : Hex.MvPoly n R cmp) : toMvPolynomial (k • p) = k • toMvPolynomial p

Conversion to Mathlib preserves natural scalar multiplication.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_pow {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) (k : ℕ) : toMvPolynomial (p ^ k) = toMvPolynomial p ^ k

Conversion to Mathlib preserves natural powers.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_natCast {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (k : ℕ) : toMvPolynomial ↑k = ↑k

Conversion to Mathlib preserves natural-number casts.

@[instance_reducible]

instance HexMvPolyMathlib.instCommSemiringMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] : CommSemiring (Hex.MvPoly n R cmp)

Mathlib's commutative-semiring structure, transported along the exact representation equivalence while retaining every executable operation.

Equations

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

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_neg {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : toMvPolynomial (-p) = -toMvPolynomial p

Forward conversion preserves coefficientwise negation.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_sub {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] [DecidableEq R] (p q : Hex.MvPoly n R cmp) : toMvPolynomial (p - q) = toMvPolynomial p - toMvPolynomial q

Forward conversion preserves subtraction.

@[implicit_reducible]

instance HexMvPolyMathlib.instIntCastMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] : IntCast (Hex.MvPoly n R cmp)

Integer casts are executable constant polynomials.

Equations

• HexMvPolyMathlib.instIntCastMvPoly = { intCast := fun (z : ℤ) => Hex.MvPoly.C ↑z }

@[implicit_reducible]

instance HexMvPolyMathlib.instSMulIntMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] : SMul ℤ (Hex.MvPoly n R cmp)

Integer scalar multiplication uses one executable constant product.

Equations

• HexMvPolyMathlib.instSMulIntMvPoly = { smul := fun (z : ℤ) (p : Hex.MvPoly n R cmp) => Hex.MvPoly.C ↑z * p }

theorem HexMvPolyMathlib.toMvPolynomial_zsmul {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] [DecidableEq R] (z : ℤ) (p : Hex.MvPoly n R cmp) : toMvPolynomial (z • p) = z • toMvPolynomial p

Conversion to Mathlib preserves integer scalar multiplication.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_intCast {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] [DecidableEq R] (z : ℤ) : toMvPolynomial ↑z = ↑z

Conversion to Mathlib preserves integer casts.

@[instance_reducible]

instance HexMvPolyMathlib.instCommRingMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommRing R] : CommRing (Hex.MvPoly n R cmp)

Mathlib's commutative-ring structure, transported along the exact representation equivalence while retaining every executable operation.

Equations

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

def HexMvPolyMathlib.constantHom {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] : R →+* Hex.MvPoly n R cmp

Executable constant polynomials packaged as a ring homomorphism.

Equations

• HexMvPolyMathlib.constantHom = { toFun := Hex.MvPoly.C, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexMvPolyMathlib.constantHom_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] (r : R) : constantHom r = Hex.MvPoly.C r

The constant homomorphism builds the executable constant polynomial.

@[implicit_reducible]

instance HexMvPolyMathlib.instAlgebraMvPoly {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] : Algebra R (Hex.MvPoly n R cmp)

The coefficient ring acts through executable constant polynomials.

Equations

• HexMvPolyMathlib.instAlgebraMvPoly = { smul := fun (r : R) (p : Hex.MvPoly n R cmp) => Hex.MvPoly.C r * p, algebraMap := HexMvPolyMathlib.constantHom, commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem HexMvPolyMathlib.algebraMap_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] (r : R) : (algebraMap R (Hex.MvPoly n R cmp)) r = Hex.MvPoly.C r

The transported algebra map is executable constant-polynomial construction.

@[simp]

theorem HexMvPolyMathlib.toMvPolynomial_smul {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (r : R) (p : Hex.MvPoly n R cmp) : toMvPolynomial (r • p) = r • toMvPolynomial p

Conversion to Mathlib preserves algebra scalar multiplication.

noncomputable def HexMvPolyMathlib.algEquiv {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] : Hex.MvPoly n R cmp ≃ₐ[R] MvPolynomial (Fin n) R

The exact representation equivalence as an equivalence of R-algebras.

Equations

• HexMvPolyMathlib.algEquiv = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem HexMvPolyMathlib.algEquiv_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : Hex.MvPoly n R cmp) : algEquiv p = toMvPolynomial p

The algebra equivalence applies as toMvPolynomial.

@[simp]

theorem HexMvPolyMathlib.algEquiv_symm_apply {n : ℕ} {R : Type u} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R] [DecidableEq R] (p : MvPolynomial (Fin n) R) : algEquiv.symm p = ofMvPolynomial p

The inverse algebra equivalence applies as ofMvPolynomial.