instCommMonoid — Mathlib

English

There is a defined addition on NumDenSameDeg 𝒜 x, given by deg, num, den as specified in the construction.

Русский

Существует определённое сложение на NumDenSameDeg 𝒜 x, заданное согласно конструкции.

LaTeX

$$$\\text{For } c_1,c_2\\colon \\mathrm{NumDenSameDeg}_{\\mathcal{A} }{x},\\; (c_1+c_2).\\deg = c_1.\\deg + c_2.\\deg,\\; (c_1+c_2).\\mathrm{num} = c_1.\\mathrm{den} \\cdot c_2.\\mathrm{num} + c_2.\\mathrm{den} \\cdot c_1.\\mathrm{num},\\; (c_1+c_2).\\mathrm{den} = c_1.\\mathrm{den} \\cdot c_2.\\mathrm{den}. $$$

Lean4

instance : CommMonoid (NumDenSameDeg 𝒜 x) where
  one := 1
  mul := (· * ·)
  mul_assoc _ _ _ := ext _ (add_assoc _ _ _) (mul_assoc _ _ _) (mul_assoc _ _ _)
  one_mul _ := ext _ (zero_add _) (one_mul _) (one_mul _)
  mul_one _ := ext _ (add_zero _) (mul_one _) (mul_one _)
  mul_comm _ _ := ext _ (add_comm _ _) (mul_comm _ _) (mul_comm _ _)

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