English
The action of a natural-number scalar commutes with an arbitrary α-action on a module.
Русский
Действие скалярного умножения на натуральное число коммутирует с действием α на модуль.
LaTeX
$$$ n \cdot (s \cdot x) = s \cdot (n \cdot x) $$$
Lean4
/-- If `E` is a vector space over a division semiring `R` and has a monoid action by `α`, then that
action commutes by scalar multiplication of inverses of natural numbers in `R`. -/
theorem inv_natCast_smul_comm {α E : Type*} (R : Type*) [AddCommMonoid E] [DivisionSemiring R] [Monoid α] [Module R E]
[DistribMulAction α E] (n : ℕ) (s : α) (x : E) : (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
(map_inv_natCast_smul (DistribMulAction.toAddMonoidHom E s) R R n x).symm
