fieldRange_castHom_eq_bot — Mathlib

English

The image of ZMod p under the canonical cast into K is the prime subfield of K (the bottom subfield).

Русский

Образ ZMod p через каноническое вложение в K равен простому подполью K (наименьшему подполю).

LaTeX

$$$\\operatorname{fieldRange}\\big( \\operatorname{ZMod.castHom}(m := p)\\, \\dvd_rfl\\, K\\big) = \\bot$$$

Lean4

theorem fieldRange_castHom_eq_bot (p : ℕ) [Fact p.Prime] [DivisionRing K] [CharP K p] :
    (ZMod.castHom (m := p) dvd_rfl K).fieldRange = (⊥ : Subfield K) := by
  rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]

Похожие утверждения