mul_of — Mathlib

English

Multiplication in MonCat.of A coincides with the original monoid multiplication.

Русский

Умножение в MonCat.of A совпадает с умножением в исходном моноиде.

LaTeX

$$$a,b:\, A\Rightarrow (@HMul.hMul (MonCat.of A)\; (MonCat.of A)\; (MonCat.of A) _ a b) = a * b$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_of {A : Type*} [Monoid A] (a b : A) : @HMul.hMul (MonCat.of A) (MonCat.of A) (MonCat.of A) _ a b = a * b :=
  rfl

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