English
If f is multipliable and i: γ → β is injective, then f ∘ i is multipliable.
Русский
Если f умножаемо и i инъективно отображает γ в β, то композиция f ∘ i тоже умножаема.
LaTeX
$$$\text{Multipliable}(f) \Rightarrow \text{Multipliable}(f\circ i)$ for injective i.$$
Lean4
@[to_additive]
theorem multipliable_of_eq_one_or_self (hf : Multipliable f) (h : ∀ b, g b = 1 ∨ g b = f b) : Multipliable g := by
classical
exact
multipliable_iff_vanishing.2 fun e he ↦
let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he
⟨s, fun t ht ↦
have eq : ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t, g b :=
calc
∏ b ∈ t with g b = f b, f b = ∏ b ∈ t with g b = f b, g b :=
Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm
_ = ∏ b ∈ t, g b := by {
refine Finset.prod_subset (Finset.filter_subset _ _) ?_
intro b hbt hb
simp only [Finset.mem_filter, and_iff_right hbt] at hb
exact (h b).resolve_right hb
}
eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩
