Theorems · Inductive type · commutative algebra

PerfectionMap

(p : ℕ) →
  [Fact (Nat.Prime p)] →
    {R : Type u₁} →
      [inst : CommSemiring R] →
        [CharP R p] → {P : Type u₂} → [inst_2 : CommSemiring P] → [CharP P p] → [PerfectRing P p] → (P →+* R) → Prop

A perfection map to a ring of characteristic p is a map that is isomorphic to its perfection.

Defined in

Mathlib.RingTheory.Perfection

Cited by

16 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

FactCommSemiringCharPCommSemiringCharPPerfectRing