annihilator_prod — Mathlib

English

The annihilator of a product is the intersection of the annihilators.

Русский

Аннигилятор произведения равен пересечению аннигиляторов составляющих.

LaTeX

$$$\\operatorname{Ann}_R(M \\times M') = \\operatorname{Ann}_R(M) \\cap \\operatorname{Ann}_R(M').$$$

Lean4

theorem annihilator_prod : annihilator R (M × M') = annihilator R M ⊓ annihilator R M' :=
  by
  ext
  simp_rw [Ideal.mem_inf, mem_annihilator, Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ←
    forall_and_right]

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