mul_def — Mathlib

English

The product in MonoidAlgebra R M is given by (x * y) = sum over all m1, m2 of x(m1) · y(m2) associated to the element m1 · m2; i.e. (x * y)(m) = sum_{m1,m2: m1 m2 = m} x(m1) y(m2).

Русский

Произведение в MonoidAlgebra R M задаётся как сумма по всем парам m1, m2: m1 m2; то есть (x * y)(m) = сумма по m1 m2 с m1 m2 = m от x(m1) y(m2).

LaTeX

$$$ (x * y)(m) = \sum_{m_1, m_2: m_1 m_2 = m} x(m_1) \cdot y(m_2) $$$

Lean4

@[to_additive (dont_translate := R) mul_def]
theorem mul_def (x y : MonoidAlgebra R M) : x * y = x.sum fun m₁ r₁ ↦ y.sum fun m₂ r₂ ↦ single (m₁ * m₂) (r₁ * r₂) := by
  with_unfolding_all rfl

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