Theorems · Theorem · commutative algebra

Perfection.pthRoot_frobenius

∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  (Perfection.pthRoot R p).comp (frobenius (Perfection R p) p) = RingHom.id (Perfection R p)

Defined in

Mathlib.RingTheory.Perfection

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringFactCharP