English
For integer cast smul, star distributes over the cast smul similarly: star(n • x) = n • star x for integer n.
Русский
Для целочисленного приведения: star(n • x) = n • star x.
LaTeX
$$$\operatorname{star}\left(n \cdot x\right) = n \cdot \operatorname{star} x$$$
Lean4
@[simp]
theorem star_ratCast_smul [DivisionRing R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ℚ) (x : M) :
star ((n : R) • x) = (n : R) • star x :=
map_ratCast_smul (starAddEquiv : M ≃+ M) _ _ _ x