smul_eq_mul — Mathlib

English

In a commutative monoid M, the action of u1 on u2 by smul coincides with multiplication: u1 • u2 = u1 u2.

Русский

В коммутативном моноиде M действие u1 над u2 через smul совпадает с умножением: u1 • u2 = u1 u2.

LaTeX

$$$ u_1, u_2 \\in M^\\times:\\; u_1 \\cdot u_2 = u_1 u_2$$$

Lean4

/-- This is not the usual `smul_eq_mul` because `mulAction'` creates a diamond.

Discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/units.2Emul_action'.20diamond/near/246400399). -/
@[simp]
theorem smul_eq_mul {M} [CommMonoid M] (u₁ u₂ : Mˣ) : u₁ • u₂ = u₁ * u₂ :=
  by
  fail_if_success
    rfl -- there is an instance diamond here

  ext
  rfl

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