prod_div_prod_mem_mulSpan — Mathlib

English

If t ⊆ s and u ⊆ s, then the quotient (∏_{a∈t} a) / (∏_{a∈u} a) lies in mulSpan(s).

Русский

Если t ⊆ s и u ⊆ s, то частное (∏_{a∈t} a) / (∏_{a∈u} a) принадлежит mulSpan(s).

LaTeX

$$((\prod_{a\in t} a) / (\prod_{a\in u} a)) \in mulSpan(s) \quad (t \subseteq s, u \subseteq s)$$

Lean4

@[to_additive]
theorem prod_div_prod_mem_mulSpan (ht : t ⊆ s) (hu : u ⊆ s) : (∏ a ∈ t, a) / ∏ a ∈ u, a ∈ mulSpan s :=
  mem_mulSpan.2
    ⟨Set.indicator t 1 - Set.indicator u 1, fun a ↦ by by_cases a ∈ t <;> by_cases a ∈ u <;> simp [*], by
      simp [prod_div_distrib, zpow_sub, ← div_eq_mul_inv, Set.indicator, pow_ite, inter_eq_right.2, *]⟩

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