star_inv_intCast_smul — Mathlib

English

For natural n, star((n⁻¹) • x) = (n⁻¹) • star x.

Русский

Для натурального n: star((n⁻¹) • x) = (n⁻¹) • star x.

LaTeX

$$$\operatorname{star}\left((n^{-1}) \cdot x\right) = (n^{-1}) \cdot \operatorname{star} x$$$

Lean4

@[simp]
theorem star_inv_intCast_smul [DivisionRing R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ℤ) (x : M) :
    star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
  map_inv_intCast_smul (starAddEquiv : M ≃+ M) R R n x

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