Theorems · Theorem · commutative algebra

Perfection.teichmullerFun_sModEq

∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsPrecomplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ},
  (Ideal.Quotient.mk I) y = (Perfection.coeff (R ⧸ I) p n) x → x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

Defined in

Mathlib.RingTheory.Teichmuller

Cited by

3 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPIsPrecomplete