English
If f is multipliable and f and g are cofinally equal (agree outside a finite set), then g is multipliable.
Русский
Если f умножаемо, и f и g совпадают за исключением конечного множества индексов, то и g является умножаемым.
LaTeX
$$$\text{Multipliable}(f) \land f =^{\mathrm{cofinite}} g \Rightarrow \text{Multipliable}(g).$$$
Lean4
/-- A more general version of `Multipliable.congr`, allowing the functions to
disagree on a finite set.
Note that this requires the target to be a group, and hence fails for products valued
in a ring. See `Multipliable.congr_cofinite₀` for a version applying in this case,
with an additional non-vanishing hypothesis.
-/
@[to_additive /-- A more general version of `Summable.congr`, allowing the functions to
disagree on a finite set. -/
]
theorem congr_cofinite (hf : Multipliable f) (hfg : f =ᶠ[cofinite] g) : Multipliable g :=
hfg.multipliable_compl_iff.mp <| (hfg.multipliable_compl_iff.mpr hf).congr (by simp)
