den_pow

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

The denominator of c^n is the n-th power of the denominator: (c^n).den = (c.den)^n.

Русский

Знаменатель c^n равен (знаменатель c)^n.

LaTeX

$$$((c^n).\\mathrm{den}) = (c.\\mathrm{den})^{n}$$$

Lean4

@[simp]
theorem den_pow (c : NumDenSameDeg 𝒜 x) (n : ℕ) : ((c ^ n).den : A) = (c.den : A) ^ n :=
  rfl

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

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

Разделы

Аффилиация

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