Theorems · Theorem · commutative algebra

DividedPowerAlgebra.lift_apply_dp

∀ {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) (n : ℕ) (m : M),
  (DividedPowerAlgebra.lift hI g hg) (DividedPowerAlgebra.dp R n m) = hI.dpow n (g m)

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringAlgebra