English
For a set s, HasProd (f restricted to s) with value a1 implies an equivalence with HasProd (f restricted to the complement) and a2, relating to a1, a2 via multiplication.
Русский
Для множества s имеет место эквивалентность между HasProd (f, ограниченной до s) с значением a1 и HasProd (f, ограниченной до дополнения) с a2 через произведение.
LaTeX
$$HasProd (f ∘ (↑) : s → α) a1 → Iff (HasProd (f ∘ (↑) : ↑sᶜ → α) a2) (HasProd f (a1 * a2))$$
Lean4
@[to_additive]
theorem hasProd_compl_iff {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) :
HasProd (f ∘ (↑) : ↑sᶜ → α) a₂ ↔ HasProd f (a₁ * a₂) :=
by
refine ⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩
rw [hasProd_subtype_iff_mulIndicator] at hf ⊢
rw [Set.mulIndicator_compl]
simpa only [div_eq_mul_inv, mul_inv_cancel_comm] using h.div hf
