toMulSemiringAction — Mathlib

English

The fixed-point subfield of a field F under a monoid M action is invariant under M.

Русский

Подполе фиксированных точек поля F относительно действия моноида M инвариантно по действию M.

LaTeX

$$$ [IsInvariantSubfield\\ M\\ S] \\Rightarrow IsInvariantSubring M S^{\\,.toSubring} $$$

Lean4

instance toMulSemiringAction [IsInvariantSubfield M S] : MulSemiringAction M S
    where
  smul m x := ⟨m • x.1, IsInvariantSubfield.smul_mem m x.2⟩
  one_smul s := Subtype.eq <| one_smul M s.1
  mul_smul m₁ m₂ s := Subtype.eq <| mul_smul m₁ m₂ s.1
  smul_add m s₁ s₂ := Subtype.eq <| smul_add m s₁.1 s₂.1
  smul_zero m := Subtype.eq <| smul_zero m
  smul_one m := Subtype.eq <| smul_one m
  smul_mul m s₁ s₂ := Subtype.eq <| smul_mul' m s₁.1 s₂.1

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