skewMonoidAlgebra — Mathlib

English

If the action of S on k is regular, then the induced action on the SkewMonoidAlgebra k G is regular as well; i.e., ha.finsupp transfers to a regular action on finsupp via ofFinsupp.

Русский

Если действие S на k регулярное, то и полученное действие на SkewMonoidAlgebra(k,G) регулярное; то есть ha.finsupp переносится на регулярное действие на finsupp через ofFinsupp.

LaTeX

$$$ IsSMulRegular(k, a) \Rightarrow IsSMulRegular( SkewMonoidAlgebra(k, G), a) $$$

Lean4

theorem _root_.IsSMulRegular.skewMonoidAlgebra {S : Type*} [Monoid S] [DistribMulAction S k] {a : S}
    (ha : IsSMulRegular k a) : IsSMulRegular (SkewMonoidAlgebra k G) a
  | ⟨_⟩, ⟨_⟩, h => by exact congr_arg _ <| ha.finsupp (ofFinsupp.inj h)

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