Theorems · Definition · commutative algebra

Submodule.pointwiseNeg

{R : Type u_2} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Neg (Submodule R M)

The submodule with every element negated. Note if R is a ring and not just a semiring, this is a no-op, as shown by Submodule.neg_eq_self. Recall that When R is the semiring corresponding to the nonnegative elements of R', Submodule R' M is the type of cones of M. This instance reflects such cones about 0. This is available as an instance in the Pointwise locale.

Defined in

Mathlib.Algebra.Module.Submodule.Pointwise

Cited by

20 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

SemiringAddCommGroupModule