multipliable_of_ne_finset_one — Mathlib

English

If f(b) = 1 for all b outside a finite set s, then f is Multipliable with respect to L.

Русский

Если вне конечного множества s все значения f равны 1, то f суммируемо по L.

LaTeX

$$$ (\forall b \notin s, f(b)=1) \rightarrow Multipliable f L $$$

Lean4

@[to_additive]
theorem multipliable_of_ne_finset_one (hf : ∀ b ∉ s, f b = 1) [L.HasSupport] : Multipliable f L := by
  classical exact (hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

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