instAddMonoid

Mathlib.RingTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.instAddMonoid

← MathLib Explorer

English

There is a negation operation on the Ore localization.

Русский

Существует операция отрицания на локализации Оре.

LaTeX

$$Neg $(X[S^{-1}])$ exists$$

Lean4

instance : AddMonoid X[S⁻¹] where
  add_assoc := OreLocalization.add_assoc
  zero_add := OreLocalization.zero_add
  add_zero := OreLocalization.add_zero
  nsmul := nsmul
  nsmul_zero _ := by with_unfolding_all rfl
  nsmul_succ _ _ := by with_unfolding_all rfl

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

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

Разделы

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

Аффилиация

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