Theorems · Theorem · logic and foundations

FirstOrder.Ring.lift_genericPolyMap

∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [inst : DecidableEq κ] [inst_1 : CommRing R] [inst_2 : DecidableEq R]
  (monoms : ι → Finset (κ →₀ ℕ)) (f : (i : ι) × ↥(monoms i) ⊕ κ → R) (i : ι),
  (FreeCommRing.lift f) (FirstOrder.Ring.genericPolyMap monoms i) =
    (MvPolynomial.eval (f ∘ Sum.inr)) (↑((FirstOrder.Ring.mvPolynomialSupportLEEquiv monoms).symm (f ∘ Sum.inl)) i)

Defined in

Mathlib.RingTheory.MvPolynomial.FreeCommRing

Cited by

2 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommRingDecidableEq