smul_mk_apply — Mathlib

English

Given m,n ∈ M and h₁,h₂ ensuring they form a unit, the action of the corresponding unit on a equals the action by m.

Русский

Пусть m,n ∈ M и h₁,h₂ задают образ еденицы; действие этой единицы на a равно действию m на a.

LaTeX

$$$ (\\langle m,n,h_1,h_2 \\rangle : M^\\times) \\; \\bullet\\; a = m \\bullet a $$$

Lean4

@[to_additive, simp]
theorem smul_mk_apply {M α : Type*} [Monoid M] [SMul M α] (m n : M) (h₁) (h₂) (a : α) :
    (⟨m, n, h₁, h₂⟩ : Mˣ) • a = m • a :=
  rfl

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