instSubsingletonSubfield — Mathlib

English

The subfield of ZMod p is a singleton: there is only one subfield.

Русский

Подполье ZMod p является одиничным: существует лишь одно подполье.

LaTeX

$$$\\operatorname{Subsingleton}\\big(\\operatorname{Subfield}(\\mathbb{Z}/p\\mathbb{Z})\\big)$$$

Lean4

instance : Subsingleton (Subfield (ZMod p)) :=
  subsingleton_of_bot_eq_top <|
    top_unique (a := ⊥) fun n _ ↦
      have := zsmul_mem (one_mem (⊥ : Subfield (ZMod p))) n.val
      by rwa [natCast_zsmul, Nat.smul_one_eq_cast, ZMod.natCast_zmod_val] at this

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