English
For AddCommMonoid M, AddCommMonoid M₂, F a FunLike M → M₂ with AddMonoidHomClass, and for division semirings R,S with M-modules over R and S, and c ∈ ℚ≥0, x ∈ M, one has f((c) • x) = (c) • f(x).
Русский
Для дополнительно коммутативной аддитивной группы M, M₂, F: M → M₂ соответствующая классу гомомордов, и для делимых полей R,S, т.к. M-модули над R и над S, при c ∈ ℚ≥0 и x ∈ M выполняется f((c) • x) = (c) • f(x).
LaTeX
$$$f((c : R) \\cdot x) = (c : S) \\cdot f(x)$$$
Lean4
theorem map_nnratCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
(f : F) (R S : Type*) [DivisionSemiring R] [DivisionSemiring S] [Module R M] [Module S M₂] (c : ℚ≥0) (x : M) :
f ((c : R) • x) = (c : S) • f x := by
rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul, map_natCast_smul f R S,
map_inv_natCast_smul f R S]
