English
If f is Multipliable, and f ≠ 0 everywhere, and f ≈ g eventually on cofinite set, then g is Multipliable.
Русский
Если f — умножимое и не обращается в нуль нигде, и f совпадает с g на кофинитной множественности, то g также умножимо.
LaTeX
$$$$ \text{Multipliable}(f) \wedge (\forall a, f(a) \neq 0) \wedge (\forall^\infty a, f(a) = g(a)) \Rightarrow \text{Multipliable}(g). $$$$
Lean4
/-- See also `Multipliable.congr_cofinite`, which does not have a non-vanishing condition, but instead
requires the target to be a group under multiplication (and hence fails for infinite products in a
ring).
-/
theorem congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠ 0) (hfg : ∀ᶠ a in cofinite, f a = g a) :
Multipliable g := by
classical
obtain ⟨c, hc⟩ := hf
obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable
