Theorems · Definition · field theory

Subalgebra.perfectClosure

(R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → (p : ℕ) → [ExpChar A p] → Subalgebra R A

The perfect closure of R in A are the elements x : A such that x ^ p ^ n is in R for some n, where p is the exponential characteristic of R.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraExpChar