instMulSemiringAction — Mathlib

English

If a group G acts on R by a MulSemiringAction, then there is a compatible action on the residue field κ(R) defined by composing the action with the induced mapAut.

Русский

Если группа G действует на R как MulSemiringAction, то существует совместимое действие на поле остатка κ(R), задаваемое через композицию действия с отображением κ.

LaTeX

$$∃MulSemiringAction G (IsLocalRing.ResidueField R) defined by (MulSemiringAction.toRingAut G R) then (mapAut ∘ MulSemiringAction.toRingAut) $$

Lean4

/-- If `G` acts on `R` as a `MulSemiringAction`, then it also acts on `IsLocalRing.ResidueField R`.
-/
noncomputable instance : MulSemiringAction G (IsLocalRing.ResidueField R) :=
  MulSemiringAction.compHom _ <| mapAut.comp (MulSemiringAction.toRingAut G R)

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