involutivePointwiseNeg — Mathlib

English

The negation operation on submodules is involutive: applying it twice returns the original submodule.

Русский

Операция отрицания подмодуля является инволюторной: дважды применяя её, получаем исходный подмодуль.

LaTeX

$$$-(-S) = S$ for all Submodule R M$$

Lean4

/-- `Submodule.pointwiseNeg` is involutive.

This is available as an instance in the `Pointwise` locale. -/
protected def involutivePointwiseNeg : InvolutiveNeg (Submodule R M)
    where
  neg := Neg.neg
  neg_neg _S := SetLike.coe_injective <| neg_neg _

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