Theorems · Theorem · field theory

PerfectClosure.mk_eq_iff

∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y : ℕ × K),
  PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔
    ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Defined in

Mathlib.FieldTheory.PerfectClosure

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingFactCharP