map_integerMultiple — Mathlib

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

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