instAdd — Mathlib

English

The denominator of the product equals the product of denominators: (pq).den = p.den · q.den.

Русский

Знаменатель произведения равен произведению знаменателей.

LaTeX

$$$(p q).\\mathrm{den} = p.\\mathrm{den} \\cdot q.\\mathrm{den}$$$

Lean4

instance : Add (NumDenSameDeg 𝒜 x) where
  add c1
    c2 :=
    { deg := c1.deg + c2.deg
      num :=
        ⟨c1.den * c2.num + c2.den * c1.num,
          add_mem (GradedMul.mul_mem c1.den.2 c2.num.2) (add_comm c2.deg c1.deg ▸ GradedMul.mul_mem c2.den.2 c1.num.2)⟩
      den := ⟨c1.den * c2.den, GradedMul.mul_mem c1.den.2 c2.den.2⟩
      den_mem := Submonoid.mul_mem _ c1.den_mem c2.den_mem }

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