English
For q ∈ ℚ, star(q • x) = q • star x.
Русский
Для q ∈ ℚ: star(q • x) = q • star x.
LaTeX
$$$\operatorname{star}(q \cdot x) = q \cdot \operatorname{star} x$$$
Lean4
/-- Note that this lemma holds for an arbitrary `ℚ`-action, rather than merely one coming from a
`DivisionRing`. We keep both the `qsmul` and `rat_smul` naming conventions for discoverability.
See `star_qsmul`. -/
@[simp high]
theorem star_rat_smul [AddCommGroup R] [StarAddMonoid R] [Module ℚ R] (q : ℚ) (x : R) : star (q • x) = q • star x :=
map_rat_smul (starAddEquiv : R ≃+ R) _ _