neg_eq_self

Mathlib.Algebra.Module.Submodule.Pointwise

URI: https://scilib.ai/kg/mathlib#Submodule.neg_eq_self

English

If the ambient ring is a ring, negation fixes a submodule exactly when the submodule is equal to its own negation.

Русский

Если кольцо, то подмодуль равен своему отрицанию тогда и только тогда, когда он равен -S.

LaTeX

$$$(-S) = S \iff S = -S$$$

Lean4

@[simp]
theorem neg_eq_self [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : -p = p :=
  ext fun _ => p.neg_mem_iff

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

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

Разделы

Аффилиация

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