Theorems · Inductive type · field theory

PerfectClosure.R

(K : Type u) → [inst : CommRing K] → (p : ℕ) → [Fact (Nat.Prime p)] → [CharP K p] → ℕ × K → ℕ × K → Prop

PerfectClosure.R is the relation (n, x) ∼ (n + 1, x ^ p) for n : ℕ and x : K. PerfectClosure K p is the quotient by this relation.

Defined in

Mathlib.FieldTheory.PerfectClosure

Cited by

8 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

CommRingFactCharP