val_neg

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

URI: https://scilib.ai/kg/mathlib#HomogeneousLocalization.val_neg

← MathLib Explorer

English

Reiterates the compatibility of val with negation: val(-y) = -val(y).

Русский

Повторяет совместимость val с отрицанием: val(-y) = -val(y).

LaTeX

$$$\mathrm{val}(-y) = -\mathrm{val}(y)$$$

Lean4

@[simp]
theorem val_neg {x} : ∀ y : HomogeneousLocalization 𝒜 x, (-y).val = -y.val :=
  Quotient.ind' fun y ↦ by rw [← mk_neg, val_mk, val_mk, Localization.neg_mk]; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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