den_add

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

URI: https://scilib.ai/kg/mathlib#HomogeneousLocalization.NumDenSameDeg.den_add

English

Repeated: (p+q).den = p.den · q.den.

Русский

Повтор: (p+q).den = p.den · q.den.

LaTeX

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

Lean4

@[simp]
theorem den_add (c1 c2 : NumDenSameDeg 𝒜 x) : ((c1 + c2).den : A) = c1.den * c2.den :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru