Theorems · Theorem · commutative algebra

IsAdicComplete.StrictMono.liftRingHom.congr_simp

∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S) {a : ℕ → ℕ}
  (ha : StrictMono a) (f f_1 : (n : ℕ) → R →+* S ⧸ I ^ a n) (e_f : f = f_1)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S],
  IsAdicComplete.StrictMono.liftRingHom I ha f hf = IsAdicComplete.StrictMono.liftRingHom I ha f_1 ⋯

Defined in

Mathlib.RingTheory.AdicCompletion.RingHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRingIsAdicComplete