_example — Mathlib

English

There is an instance IsCyclotomicExtension for singleton {n} over K, with CyclotomicField n K.

Русский

Существует инстанс IsCyclotomicExtension для одинокого множества {n} над K и CyclotomicField n K.

LaTeX

$$$IsCyclotomicExtension\\{n\\} K (CyclotomicField n K)$$$

Lean4

/--
Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -/
example : Ring.toIntAlgebra (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ :=
  rfl

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