English
For a group G acting on α, the inverse action cancels the forward action: g⁻¹ • g • a = a.
Русский
Для группы G, действующей на α, обратное действие отменяет прямое: g⁻¹ • g • a = a.
LaTeX
$$$\\\\forall g \\\\in G, \\\\forall a \\\\in α, \\\\ g^{-1} \\\\cdot g \\\\cdot a = a.$$$
Lean4
/-- Pullback a multiplicative action along an injective map respecting `•`.
See note [reducible non-instances]. -/
@[to_additive /-- Pullback an additive action along an injective map respecting `+ᵥ`. -/
]
protected abbrev mulAction [SMul M β] (f : β → α) (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
MulAction M β where
smul := (· • ·)
one_smul x := hf <| (smul _ _).trans <| one_smul _ (f x)
mul_smul c₁ c₂ x := hf <| by simp only [smul, mul_smul]
