mul_sub_mul_mem — Mathlib

English

If I is a two-sided ideal and a−b ∈ I and c−d ∈ I, then ac−bd ∈ I.

Русский

Если I — двусторонний идеал и A−B ∈ I, C−D ∈ I, то AC−BD ∈ I.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha)\; \forall a,b,c,d:\alpha, \; (a-b)\in I \land (c-d)\in I \Rightarrow (ac-bd)\in I.$$$

Lean4

theorem mul_sub_mul_mem [I.IsTwoSided] (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I :=
  by
  rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]
  exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)

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