hasDistribPointwiseNeg — Mathlib

English

Submodules carry a pointwise negation compatible with multiplication, i.e., negation distributes over the product.

Русский

Подмодули образуют точечную отрицательную структуру с совместимой с умножением дистрибутивностью отрицания.

LaTeX

$$$\\text{HasDistribNeg} \\; (\\mathrm{Submodule}\\; R\\; A)$$$

Lean4

/-- `Submodule.pointwiseNeg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale. -/
protected def hasDistribPointwiseNeg {A} [Ring A] [Algebra R A] : HasDistribNeg (Submodule R A) :=
  toAddSubmonoid_injective.hasDistribNeg _ neg_toAddSubmonoid mul_toAddSubmonoid

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