star_rat_smul — Mathlib

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) _ _

Похожие утверждения