finSepDegree_self — Mathlib

English

The finite separable degree of a field over itself is 1: finSepDegree F F = 1.

Русский

Конечная разделяемая степень поля над самим собой равна 1.

LaTeX

$$$\\operatorname{finSepDegree} F F = 1$$$

Lean4

@[simp]
theorem finSepDegree_self : finSepDegree F F = 1 :=
  by
  have : Cardinal.mk (Emb F F) = 1 :=
    le_antisymm (Cardinal.le_one_iff_subsingleton.2 AlgHom.subsingleton)
      (Cardinal.one_le_iff_ne_zero.2 <| Cardinal.mk_ne_zero _)
  rw [finSepDegree, Nat.card, this, Cardinal.one_toNat]

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