English
The image of the integerMultiple under f is exactly the product of the common denominator with the corresponding g i.
Русский
Образ integerMultiple под f равен произведению общего знаменателя на соответствующий g i.
LaTeX
$$$\text{Eq}(\mathrm{LinearMap.instFunLike.coe}\,f\, (\mathrm{IsLocalizedModule.integerMultiple}(S,f,s,g,i)), \mathrm{IsLocalizedModule.IsInteger}.?)$$$
Lean4
@[simp]
theorem map_integerMultiple {ι : Type*} (s : Finset ι) (g : ι → M') (i : s) :
f (integerMultiple S f s g i) = commonDenom S f s g • g i :=
((exist_integer_multiples S f s g).choose_spec _ i.prop).choose_spec