instNeg

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

English

The degree component behaves oppositely under negation, keeping its value unchanged in degree.

Русский

Степенная часть сохраняет своё значение под отрицанием в отношении степени.

LaTeX

$$$$ (-c).deg = c.deg. $$$$

Lean4

instance : Neg (NumDenSameDeg 𝒜 x) where neg c := ⟨c.deg, ⟨-c.num, neg_mem c.num.2⟩, c.den, c.den_mem⟩

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

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

Разделы

Аффилиация

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