mul_neg_mem — Mathlib

English

An instance shows that a nonunital subsemiring induces the MulMemClass structure, i.e., closure under multiplication by ring elements from both sides.

Русский

Инстанс показывает, что неединичное подполье индицирует структуру MulMemClass, то есть замыкание под произведением слева и справа от элементов кольца.

LaTeX

$$MulMemClass S R$$

Lean4

/-- 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. -/
@[aesop unsafe 80% (rule_sets := [SetLike])]
theorem mul_neg_mem {x y : R} (hx : x ∈ s) (hy : -y ∈ s) : -(x * y) ∈ s := by simpa using mul_mem hx hy

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