English
Star distributes over rational cast smul: star((n : R) • x) = (n : R) • star x for n ∈ ℚ.
Русский
Звезда распределяется через рациональное приведение: star((n : R) • x) = (n : R) • star x, n ∈ ℚ.
LaTeX
$$$\operatorname{star}\left((n : \mathbb{Q}) \cdot x\right) = (n : \mathbb{Q}) \cdot \operatorname{star} x$$$
Lean4
/-- Note that this lemma holds for an arbitrary `ℚ≥0`-action, rather than merely one coming from a
`DivisionSemiring`. We keep both the `nnqsmul` and `nnrat_smul` naming conventions for
discoverability. See `star_nnqsmul`. -/
@[simp high]
theorem star_nnrat_smul [AddCommMonoid R] [StarAddMonoid R] [Module ℚ≥0 R] (q : ℚ≥0) (x : R) :
star (q • x) = q • star x :=
map_nnrat_smul (starAddEquiv : R ≃+ R) _ _
