English
If S ⊆ R is an invariant subring under M, then S carries an induced MulSemiringAction of M via smul m x = ⟨m • x, proof⟩, with the structure inherited from R.
Русский
Если S ⊆ R — инвариантное подполье относительно M, то на S действует индуцированное MulSemiringAction: smul m x = ⟨m • x, доказательство⟩, структура унаследована от R.
LaTeX
$$$[IsInvariantSubring M S] \\Rightarrow \\text{MulSemiringAction } M S$ with $smul\\; m\\; x = ⟨m\\cdot x, \\ IsInvariantSubring.smul_mem m x.2⟩$$$
Lean4
instance toMulSemiringAction [IsInvariantSubring M S] : MulSemiringAction M S
where
smul m x := ⟨m • ↑x, IsInvariantSubring.smul_mem m x.2⟩
one_smul s := Subtype.eq <| one_smul M (s : R)
mul_smul m₁ m₂ s := Subtype.eq <| mul_smul m₁ m₂ (s : R)
smul_add m s₁ s₂ := Subtype.eq <| smul_add m (s₁ : R) (s₂ : R)
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₁ : R) (s₂ : R)
