mem_bot_iff_intCast — Mathlib

English

In a field K of characteristic p, an element x lies in the prime subfield ⊥ if and only if x equals an integer.

Русский

В поле K характеристика p, элемент x лежит в простом подполе ⊥ тогда и только тогда, когда x равно целому числу.

LaTeX

$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\Rightarrow \\\\forall K \\\\text{with Characteristic } p, x \\\\in \\⊥ \\\\Leftrightarrow \\\\exists n \\\\in \\\\mathbb{Z}, n = x$$$

Lean4

theorem mem_bot_iff_intCast (p : ℕ) [Fact p.Prime] (K) [DivisionRing K] [CharP K p] {x : K} :
    x ∈ (⊥ : Subfield K) ↔ ∃ n : ℤ, n = x := by simp [← fieldRange_castHom_eq_bot p, ZMod.intCast_surjective.exists]

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