smul — Mathlib

English

The action is given by a compatible scalar multiplication: for ϕ ∈ p.Gal and x ∈ rootSet p E, ϕ • x is defined via the root-equivalence map.

Русский

Действие задаётся согласованной умножением на скаляры: для ϕ ∈ p.Gal и x ∈ rootSet p E скалярное умножение ϕ • x определяется через отображение, связывающее корни.

LaTeX

$$$\\forall ϕ\\in p.Gal, x\\in rootSet(p,E): ϕ\\cdot x = \\mathrm{rootsEquivRoots}(p,E)(ϕ\\cdot (\\mathrm{rootsEquivRoots}(p,E))^{-1} x)$$$

Lean4

instance smul [Fact (p.Splits (algebraMap F E))] : SMul p.Gal (rootSet p E) where
  smul ϕ x := rootsEquivRoots p E (ϕ • (rootsEquivRoots p E).symm x)

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