mem_span_mul_finite_of_mem_mul — Mathlib

English

If x ∈ I·J, then there exist Finsets T and T' with T ⊆ I and T' ⊆ J such that x ∈ span_R (T · T').

Русский

Если x ∈ I·J, существуют конечные множества T, T' такие, что T ⊆ I, T' ⊆ J и x ∈ span_R(T·T').

LaTeX

$$$ x \\in I \\cdot J \\Rightarrow \\exists T,T' \\subseteq P, (T:Set P) \\subseteq I, (T':Set P) \\subseteq J, x \\in \\mathrm{span}_R (T \\cdot T') $$$

Lean4

theorem mem_span_mul_finite_of_mem_mul {I J : FractionalIdeal S P} {x : P} (hx : x ∈ I * J) :
    ∃ T T' : Finset P, (T : Set P) ⊆ I ∧ (T' : Set P) ⊆ J ∧ x ∈ span R (T * T' : Set P) :=
  Submodule.mem_span_mul_finite_of_mem_mul (by simpa using mem_coe.mpr hx)

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