Theorems · Theorem · commutative algebra

Perfection.hom_ext

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u₁} [inst : CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂}
  [inst_3 : CommSemiring S] [inst_4 : CharP S p] {f g : R →+* Perfection S p},
  (∀ (x : R), (Perfection.coeff S p 0) (f x) = (Perfection.coeff S p 0) (g x)) → f = g

Defined in

Mathlib.RingTheory.Perfection

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCommSemiringCharPPerfectRingCommSemiringCharP