quotient — Mathlib

English

There is a natural quotient action of β on the quotient HasQuotient.Quotient α H given by b • [a] = [b a].

Русский

Существует естественное квотиентное действие β на квадринутый набор G/H, заданное $b\\cdot [a] = [b a]$.

LaTeX

$$$(b, [a]) \\mapsto [b a]$$$

Lean4

@[to_additive]
instance quotient [QuotientAction β H] : MulAction β (α ⧸ H)
    where
  smul b := Quotient.map' (b • ·) fun _ _ h => leftRel_apply.mpr <| QuotientAction.inv_mul_mem b <| leftRel_apply.mp h
  one_smul q := Quotient.inductionOn' q fun a => congr_arg Quotient.mk'' (one_smul β a)
  mul_smul b b' q := Quotient.inductionOn' q fun a => congr_arg Quotient.mk'' (mul_smul b b' a)

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