English
The cast from Rat to the base ring acts linearly with respect to smul on modules, i.e., a·(q • x) = q • (a·x) for a ∈ Rat, q ∈ R, x in the module.
Русский
Приведение из Rat в основание кольца действует линейно относительно смула на модулях: a · (q • x) = q • (a · x).
LaTeX
$$$$ a \\cdot (q \\cdot x) = q \\cdot (a \\cdot x) $$$$
Lean4
/-- `qsmul` is equal to any other module structure via a cast. -/
theorem cast_smul_eq_qsmul [Module R S] (q : ℚ) (a : S) : (q : R) • a = q • a :=
by
refine MulAction.injective₀ (G₀ := ℚ) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
dsimp
rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Int.cast_smul_eq_zsmul, ← smul_assoc, nsmul_eq_mul q.den, ←
cast_natCast, ← cast_mul, den_mul_eq_num, cast_intCast, Int.cast_smul_eq_zsmul]
