Theorems · Theorem · commutative algebra

DividedPowerAlgebra.lift_apply

∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A}
  (hg : ∀ (m : M), g m ∈ I) (p : MvPolynomial (ℕ × M) R),
  (DividedPowerAlgebra.lift hI g hg) ↑p = (MvPolynomial.aeval fun nm => hI.dpow nm.1 (g nm.2)) p

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringAlgebra