Theorems · Theorem · field theory

Subfield.bot_eq_of_zMod_algebra

∀ {K : Type u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] [inst : Field K] [inst_1 : Algebra (ZMod p) K],
  ⊥ = (algebraMap (ZMod p) K).fieldRange

The smallest subfield of a field of characteristic p is (the image of) ZMod p. Note that the fact that the field K is of characteristic p is stated by the fact that it is ZMod p-algebra.

Defined in

Mathlib.FieldTheory.PrimeField

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactFieldAlgebra