coe_mulₗᵢ — Mathlib

English

The flip of multiplication is the same as multiplication for the underlying structure; i.e., reversed order remains multiplication.

Русский

Перевернутое умножение совпадает с обычным умножением в базовой структуре; порядок перемножения не изменяет операцию.

LaTeX

$$$(\mathrm{mul}\; \cdot)^{\text{flip}} = \mathrm{mul}$$$

Lean4

@[simp]
theorem coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 R) = mul 𝕜 R :=
  rfl

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