instGroupWithZero — Mathlib

English

The splitting field carries a natural group with zero structure induced by its algebraic operations.

Русский

Разворачивающее поле оснащено естественной структурой группы с нулём, порождаемой его алгебраическими операциями.

LaTeX

$$$\\text{GroupWithZero }(\\text{SplittingField }f)$$$

Lean4

instance instGroupWithZero : GroupWithZero (SplittingField f) :=
  let e := algEquivSplittingFieldAux f
  { inv := fun a ↦ e.symm (e a)⁻¹
    inv_zero := by simp
    mul_inv_cancel := fun a ha ↦ e.injective <| by simp [EmbeddingLike.map_ne_zero_iff.2 ha]
    __ := e.surjective.nontrivial }

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