Theorems · Theorem · ring theory

mul_neg_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

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MulHasDistribNegSetLikeMulMemClass