Theorems · Definition · commutative algebra

PreTilt.coeff

{O : Type u₂} →
  [inst : CommRing O] →
    {p : ℕ} → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : Fact ¬IsUnit ↑p] → ℕ → PreTilt O p →+* ModP O p

The n-th coefficient of an element of the perfection of O/(p).

Defined in

Mathlib.RingTheory.Perfection

Cited by

21 results in Mathlib

Foundations

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

Assumes

CommRingFactFact