English
If E is a vector space over a division ring and equipped with a module action by α, then the α-action commutes with inverses of integers in the division ring.
Русский
Если E — векторное пространство над кольцом деления и имеется действие α, то это действие коммутирует с обратными числами целых через деление.
LaTeX
$$$ (n^{-1}) \cdot (s \cdot x) = s \cdot (n^{-1} \cdot x) $$$
Lean4
/-- If `E` is a vector space over a division ring `R` and has a monoid action by `α`, then that
action commutes by scalar multiplication of inverses of integers in `R` -/
theorem inv_intCast_smul_comm {α E : Type*} (R : Type*) [AddCommGroup E] [DivisionRing R] [Monoid α] [Module R E]
[DistribMulAction α E] (n : ℤ) (s : α) (x : E) : (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
(map_inv_intCast_smul (DistribMulAction.toAddMonoidHom E s) R R n x).symm
