num_neg

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

Two degree-parts of homogeneous localization are equal if their deg, num, and den match.

Русский

Две части степеней локализации одинаковы, если совпадают deg, num и den.

LaTeX

$$$$ \text{ext}(c_1, c_2) \Rightarrow c_1 = c_2. $$$$

Lean4

@[simp]
theorem num_neg (c : NumDenSameDeg 𝒜 x) : ((-c).num : A) = -c.num :=
  rfl

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

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

Разделы

Аффилиация

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