Theorems · Definition · commutative algebra

Perfection.teichmullerCauchy

{p : ℕ} →
  [Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst : CommRing R] →
        {I : Ideal R} → [CharP (R ⧸ I) p] → Perfection (R ⧸ I) p → AdicCompletion.AdicCauchySequence I R

teichmullerAux as an adic Cauchy sequence.

Defined in: Mathlib.RingTheory.Teichmuller
Cited by: 1 results in Mathlib
Foundations: Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact CommRing CharP

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Idealstatement and proof · cited by 4,748
Factstatement and proof · cited by 2,726
HasQuotient.Quotientstatement and proof · cited by 2,301
Nat.Primestatement and proof · cited by 2,059
CharPstatement and proof · cited by 478
Perfectionstatement and proof · cited by 84
AdicCompletion.AdicCauchySequencestatement · cited by 41
Perfection.teichmullerAuxproof · cited by 4
AdicCompletion.AdicCauchySequence.mkproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

Perfection.exists_teichmullerFunproof · cited by 1