Theorems · Theorem · commutative algebra

AdicCompletion.factor_eval_liftRingHom

∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m)
  (n : ℕ) (x : R) (h : I ^ n • ⊤ ≤ I ^ n),
  (Submodule.factor h) ((AdicCompletion.eval I S n) ((AdicCompletion.liftRingHom I f ⋯) x)) = (f n) x

Defined in

Mathlib.RingTheory.AdicCompletion.Algebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRing