star_inv_natCast_smul — Mathlib

English

For any NNReal-valued action of a additive monoid R on M, star distributes over q- scaled elements with q in ℚ≥0: star(q • x) = q • star x.

Русский

Для действия NNReal над R на M справедливо: star(q • x) = q • star x, при q ∈ ℚ≥0.

LaTeX

$$$\text{star}_{NNRat}\;\text{smul}: \star(q \cdot x) = q \cdot \star x\quad (q \in \mathbb{Q}_{\ge 0})$$$

Lean4

@[simp]
theorem star_inv_natCast_smul [DivisionSemiring R] [AddCommMonoid M] [Module R M] [StarAddMonoid M] (n : ℕ) (x : M) :
    star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
  map_inv_natCast_smul (starAddEquiv : M ≃+ M) R R n x

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