Theorems · Definition · field theory

PerfectClosure.liftOn

{K : Type u} →
  [inst : CommRing K] →
    {p : ℕ} →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : CharP K p] →
          {L : Type u_1} →
            PerfectClosure K p → (f : ℕ × K → L) → (∀ (x y : ℕ × K), PerfectClosure.R K p x y → f x = f y) → L

Lift a function ℕ × K → L to a function on PerfectClosure K p.

Defined in

Mathlib.FieldTheory.PerfectClosure

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

CommRingFactCharP