ofMulAction_apply — Mathlib

English

The action defined on the carrier of H by MulAction coincides with the given action: (FintypeCat.ofMulAction G H).ρ g x = (g • x).

Русский

Действие на носителе H, определённое MulAction, совпадает с заданным действием: (FintypeCat.ofMulAction G H).ρ g x = g • x.

LaTeX

$$$ (FintypeCat.ofMulAction G H).\rho g x = (g \cdot x) $$$

Lean4

@[simp]
theorem ofMulAction_apply {G : Type*} {H : FintypeCat.{u}} [Monoid G] [MulAction G H] (g : G) (x : H) :
    (FintypeCat.ofMulAction G H).ρ g x = (g • x : H) :=
  rfl

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