negSelf

Mathlib.GroupTheory.MonoidLocalization.Away

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.LocalizationMap.AwayMap.negSelf

Lean4

/-- Given `x : A` and a Localization map `F : A →+ B` away from `x`, `neg_self` is `- (F x)`. -/
noncomputable def negSelf : B :=
  F.mk' 0 ⟨x, mem_multiples _⟩

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

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

Разделы

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

Аффилиация

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