star_ratCast_smul — Mathlib

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

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