applyMulSemiringAction — Mathlib

English

There is a natural MulSemiringAction of Gal(p) on p.SplittingField, given by the obvious action of automorphisms on the splitting field.

Русский

Существует естественное действие MulSemiringAction Гал(p) на p.SplittingField, задаваемое действием автоморфизмов на поле разложения.

LaTeX

$$$\text{instance } \text{applyMulSemiringAction}: \mathrm{MulSemiringAction}\ p.Gal\ p.SplittingField.$$$

Lean4

instance applyMulSemiringAction : MulSemiringAction p.Gal p.SplittingField :=
  AlgEquiv.applyMulSemiringAction

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