prod_sdiff_eq_div — Mathlib

English

If s1 ⊆ s2, then ∏ x ∈ s2 \\ s1 f x = (∏ x ∈ s2 f x) / (∏ x ∈ s1 f x).

Русский

Если s1 ⊆ s2, то ∏ x ∈ s2 \\ s1 f x = (∏ x ∈ s2 f x) / (∏ x ∈ s1 f x).

LaTeX

$$$$ \\prod_{x \\in s_2 \\setminus s_1} f(x) = \\frac{\\prod_{x \\in s_2} f(x)}{\\prod_{x \\in s_1} f(x)} $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_sdiff_eq_div (h : s₁ ⊆ s₂) : ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x := by
  rw [eq_div_iff_mul_eq', prod_sdiff h]

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