Theorems · Theorem · commutative algebra

Perfection.ext

∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {f g : Perfection R p},
  (∀ (n : ℕ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g) → f = g

Defined in

Mathlib.RingTheory.Perfection

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringFactCharP