smul_mk — Mathlib

English

On the quotient α/H there is a β-action compatible with the quotient map, i.e., b • [a] = [b • a].

Русский

На фактор-множестве α/H имеется действие β, совместимое с квотами: b • [a] = [b • a].

LaTeX

$$$b \\cdot \\operatorname{QuotientGroup.mk} a = \\operatorname{QuotientGroup.mk} (b \\cdot a)$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_mk [QuotientAction β H] (b : β) (a : α) : (b • QuotientGroup.mk a : α ⧸ H) = QuotientGroup.mk (b • a) :=
  rfl

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