English
If f is injective, then comapDomain with f commutes with scalar multiplication: comapDomain f (r • v) hf.injOn = r • comapDomain f v hf.injOn.
Русский
Если f инъективно, то comapDomain сохраняет скалярное умножение: comapDomain f (r • v) hf.injOn = r • comapDomain f v hf.injOn.
LaTeX
$$$[Zero M][SMulZeroClass R M] {f : \\alpha \\to \\beta} (hf : Function.Injective f) (r : R) (v : \\beta \\to_0 M) :\n comapDomain f (r \\cdot v) hf.injOn = r \\cdot comapDomain f v hf.injOn$$$
Lean4
/-- A version of `Finsupp.comapDomain_smul` that's easier to use. -/
theorem comapDomain_smul_of_injective [Zero M] [SMulZeroClass R M] {f : α → β} (hf : Function.Injective f) (r : R)
(v : β →₀ M) : comapDomain f (r • v) hf.injOn = r • comapDomain f v hf.injOn :=
comapDomain_smul _ _ _ _
