English
For any q ∈ ℚ≥0 and a ∈ S, the scalar action of q viewed as an element of R on a equals the ℚ≥0-smul action: (q : R) • a = q • a.
Русский
При любом q ∈ ℚ≥0 и a ∈ S действие скаляра, полученное путём приведения q к R, совпадает с исходным ℚ≥0-калярным действием: (q : R) • a = q • a.
LaTeX
$$$$ (q : R) \\cdot a = q \\cdot a $$$$
Lean4
/-- `nnqsmul` is equal to any other module structure via a cast. -/
theorem cast_smul_eq_nnqsmul [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a :=
by
refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
dsimp
rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, ← smul_assoc, nsmul_eq_mul q.den, ←
cast_natCast, ← cast_mul, den_mul_eq_num, cast_natCast, Nat.cast_smul_eq_nsmul]
