single_mul_single — Mathlib

English

The product of basis elements satisfies single m1 r1 * single m2 r2 = single (m1 m2) (r1 r2).

Русский

Произведение базисных элементов даёт снова базисный элемент: single(m1,r1) · single(m2,r2) = single(m1 m2, r1 r2).

LaTeX

$$$\operatorname{single}(m_1,r_1) \cdot \operatorname{single}(m_2,r_2) = \operatorname{single}(m_1 m_2, r_1 r_2)$$$

Lean4

@[to_additive (attr := simp) (dont_translate := R) single_mul_single]
theorem single_mul_single (m₁ m₂ : M) (r₁ r₂ : R) : single m₁ r₁ * single m₂ r₂ = single (m₁ * m₂) (r₁ * r₂) := by
  simp [mul_def]

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