instCommSemiring — Mathlib

English

The product of two monomials is a monomial with exponent m+n and coefficient a b.

Русский

Произведение двух мономиалов равно мономиалу с экспонентой m+n и коэффициентом ab.

LaTeX

$$$$ \operatorname{monomial}(m,a) \cdot \operatorname{monomial}(n,b) = \operatorname{monomial}(m+n, ab) $$$$

Lean4

instance [CommSemiring R] : CommSemiring (MvPowerSeries σ R) :=
  { show Semiring (MvPowerSeries σ R) by infer_instance with
    mul_comm := fun φ ψ =>
      ext fun n => by
        classical simpa only [coeff_mul, mul_comm] using sum_antidiagonal_swap n fun a b => coeff a φ * coeff b ψ }

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