instMul — Mathlib

English

The degree of the product of two fractions adds the degrees: deg(pq) = deg(p) + deg(q).

Русский

Степень произведения двух дробей равна сумме степеней: deg(pq) = deg(p) + deg(q).

LaTeX

$$$\\deg(p q) = \\deg(p) + \\deg(q)$$$

Lean4

instance : Mul (NumDenSameDeg 𝒜 x) where
  mul p
    q :=
    { deg := p.deg + q.deg
      num := ⟨p.num * q.num, mul_mem p.num.prop q.num.prop⟩
      den := ⟨p.den * q.den, mul_mem p.den.prop q.den.prop⟩
      den_mem := Submonoid.mul_mem _ p.den_mem q.den_mem }

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