neg_mul_mem — Mathlib

English

If -x ∈ s and y ∈ s, then -(x y) ∈ s; i.e., closure under negation plus multiplication implies closure under negated products.

Русский

Если -x ∈ s и y ∈ s, то -(x y) ∈ s; т.е. замыкание по отрицанию и умножению даёт замыкание по произведению с отрицанием.

LaTeX

$${x y : R} (hx : -x ∈ s) (hy : y ∈ s) : -(x * y) ∈ s$$

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 neg_mul_mem {x y : R} (hx : -x ∈ s) (hy : y ∈ s) : -(x * y) ∈ s := by simpa using mul_mem hx hy

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