annihilator_pi — Mathlib

English

The annihilator of a Pi-type product agrees with the infimum of the annihilators of each factor.

Русский

Аннигилятор произведения типа Pi совпадает с наименьшим пересечением аннигиляторов каждого множителя.

LaTeX

$$$ \\operatorname{Ann}_R\\Big(\\prod_i M_i\\Big) = \\bigcap_i \\operatorname{Ann}_R(M_i). $$$

Lean4

theorem annihilator_pi : annihilator R (Π i, M i) = ⨅ i, annihilator R (M i) :=
  by
  ext r; simp only [mem_annihilator, Ideal.mem_iInf]
  constructor <;> intro h
  · intro i m
    classical simpa using congr_fun (h (Pi.single i m)) i
  · intro m; ext i; exact h i _

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