ne_bot_of_prod_finsetApprox_mem — Mathlib

English

MkMMem is a specialization of mk0 to the finite set of ideals that contain M = ∏ m ∈ finsetApprox(bS, adm). It assigns to a given ideal J the class of an ideal J' whose quotient by the nonzero-divisors matches J and which contains M.

Русский

mkMMem является специализированной версией mk0 на конечное множество идеалов, содержащих M = ∏ m ∈ finsetApprox(bS, adm). Он сопоставляет данному J класс mk0(J'), где J' удовлетворяет условиям.

LaTeX

$$$ \\mathrm{mkMMem}(b_S, adm)(J) = \\mathrm{mk0}(J') \\quad\\text{для некоторого } J' \\text{ с } M \\in J' \\text{ и } J' \\text{ удовлетворяет условиям }$$

Lean4

theorem ne_bot_of_prod_finsetApprox_mem (J : Ideal S) (h : algebraMap _ _ (∏ m ∈ finsetApprox bS adm, m) ∈ J) : J ≠ ⊥ :=
  (Submodule.ne_bot_iff _).mpr ⟨_, h, prod_finsetApprox_ne_zero _ _⟩

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