prod_finsetApprox_ne_zero — Mathlib

English

If a nonzero divisor product M = ∏ m ∈ finsetApprox(bS, adm) lies in an ideal J of S, then J is not the zero ideal.

Русский

Если произведение M = ∏ м из finsetApprox(bS, adm) принадлежит идеалу J в S и является не нулевым делителем, то J не равно нулю.

LaTeX

$$$ J \\neq \\{0\\} \\quad\\text{if } algebraMap_R_S(M) \\in J, \\text{ with } M = \\prod_{m \\in \\mathrm{finsetApprox}(b_S, adm)} m $$$

Lean4

theorem prod_finsetApprox_ne_zero : algebraMap R S (∏ m ∈ finsetApprox bS adm, m) ≠ 0 :=
  by
  refine mt ((injective_iff_map_eq_zero _).mp bS.algebraMap_injective _) ?_
  simp only [Finset.prod_eq_zero_iff, not_exists]
  rintro x ⟨hx, rfl⟩
  exact finsetApprox.zero_notMem bS adm hx

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