num_smul

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

Multiplication by a scalar on the numerator scales the numerator accordingly.

Русский

Умножение числителя на скаляр масштабирует числитель соответственно.

LaTeX

$$$$ (m \cdot c).num = m \cdot c.num. $$$$

Lean4

@[simp]
theorem num_smul (c : NumDenSameDeg 𝒜 x) (m : α) : ((m • c).num : A) = m • c.num :=
  rfl

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

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

Разделы

Аффилиация

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