den_mul

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

Repeated assertion: num((p q)) = p.num q.num.

Русский

Повтор: num(p q) = num(p) num(q).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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