English
Let AddCommGroup M and M₂, with F: Type* → M → M₂ FunLike and AddMonoidHomClass F M M₂. For R,S DivisionRing, Modules R M, S M₂, and c ∈ ℚ, x ∈ M, we have f((c) • x) = (c) • f(x).
Русский
Пусть M и M₂ — AddCommGroup, F: Type* → M → M₂ линейно, R и S — DivisionRing, M ⊣ R-модуль и M₂ ⊣ S-модуль. Тогда для c ∈ ℚ и x ∈ M выполняется f((c) • x) = (c) • f(x).
LaTeX
$$$f((c : R) \\cdot x) = (c : S) \\cdot f(x)$$$
Lean4
theorem map_ratCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
(f : F) (R S : Type*) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (c : ℚ) (x : M) :
f ((c : R) • x) = (c : S) • f x := by
rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul, map_intCast_smul f R S,
map_inv_natCast_smul f R S]
