instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra

English

The quotient action inherits SMulCommClass: the quotient action on fixed subalgebras commutes with scalar multiplication from A.

Русский

Действие по фактор-группе сохраняет SMulCommClass: квадратно-подгруппа действует, и умножение на скаляры от A коммутирует.

LaTeX

$$$\text{SMulCommClass } (G/H) A (FixedPoints.subalgebra\; A\; B\; H).$$$

Lean4

instance (H : Subgroup G) [H.Normal] : SMulCommClass (G ⧸ H) A (FixedPoints.subalgebra A B H) where
  smul_comm := Quotient.ind fun g r h ↦ Subtype.ext (smul_comm g r h.1)

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