instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra

English

There is a natural MulSemiringAction of G/H on FixedPoints.subring B H when H is normal.

Русский

Существует естественное действие MulSemiringAction группы G/H на FixedPoints.subring B H при H нормальной.

LaTeX

$$$\text{Given } H \triangleleft G,\; \text{ MulSemiringAction } (G/H) \;\text{on } FixedPoints.subring B H.$$$

Lean4

instance (H : Subgroup G) [H.Normal] : MulSemiringAction (G ⧸ H) (FixedPoints.subalgebra A B H) :=
  inferInstanceAs (MulSemiringAction (G ⧸ H) (FixedPoints.subring B H))

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