instIsScalarTowerCyclotomicField — Mathlib

English

There is a natural tower of scalars A → CyclotomicRing n A K → CyclotomicField n K, i.e. the two-step scalar action satisfies compatibility: (a·r)·s = a·(r·s) for a ∈ A, r ∈ CyclotomicRing n A K, s ∈ CyclotomicField n K.

Русский

Существуют скаляры A → CyclotomicRing n A K → CyclotomicField n K образуют цепь скаляров: (a·r)·s = a·(r·s) для a ∈ A, r ∈ CyclotomicRing n A K, s ∈ CyclotomicField n K.

LaTeX

$$$\\forall a\\in A,\\; \\forall r\\in \\operatorname{CyclotomicRing}(n,A,K),\\; \\forall s\\in \\operatorname{CyclotomicField}(n,K),\\; (a\\cdot r)\\cdot s = a\\cdot (r\\cdot s)$$$

Lean4

instance : IsScalarTower A (CyclotomicRing n A K) (CyclotomicField n K) :=
  IsScalarTower.subalgebra' _ _ _ _

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