smul_def — Mathlib

English

The smul operation on rootSet p E is definitional: ϕ • x equals rootsEquivRoots(p,E) (ϕ • (rootsEquivRoots(p,E))^{-1} x).

Русский

Операция умножения на элемент группы на множество корней определяется дефиниционально через эквивалентность корней.

LaTeX

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

Lean4

theorem smul_def [Fact (p.Splits (algebraMap F E))] (ϕ : p.Gal) (x : rootSet p E) :
    ϕ • x = rootsEquivRoots p E (ϕ • (rootsEquivRoots p E).symm x) :=
  rfl

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