Theorems · Theorem · commutative algebra

Perfection.lift_symm_apply

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [inst : CommSemiring R] [inst_1 : CharP R p]
  [inst_2 : PerfectRing R p] (S : Type u₂) [inst_3 : CommSemiring S] [inst_4 : CharP S p] (f : R →+* Perfection S p),
  (Perfection.lift p R S).symm f = (Perfection.coeff S p 0).comp f

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