Theorems · Theorem · ring theory

neg_mul_mem

∀ {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst_1 : HasDistribNeg R] [inst_2 : SetLike S R] [MulMemClass S R]
  {s : S} {x y : R}, -x ∈ s → y ∈ s → -(x * y) ∈ s

This lemma exists for aesop, as aesop simplifies -x * y to -(x * y) before applying unsafe rules like mul_mem, leading to a dead end in cases where neg_mem does not hold.

Defined in

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MulHasDistribNegSetLikeMulMemClass