num_mul

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

The numerator of the product equals the product of numerators: (pq).num = p.num · q.num.

Русский

Числитель произведения равен произведению числителей.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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