mul' — Mathlib

English

Multiplication on polynomials is the standard polynomial multiplication, i.e., the product in the polynomial ring equals the usual Cauchy product.

Русский

Умножение полиномов — обычное умножение полиномов, то есть произведение в кольце полиномов.

LaTeX

$$$ \text{mul}' = \cdot $$$

Lean4

instance mul' : Mul R[X] :=
  ⟨mul⟩
    -- If the private definitions are accidentally exposed, simplify them away.

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