Theorems · Theorem · commutative algebra

inv_intCast_smul_comm

∀ {α : Type u_5} {E : Type u_6} (R : Type u_7) [inst : AddCommGroup E] [inst_1 : DivisionRing R] [inst_2 : Module R E]
  [inst_3 : DistribSMul α E] (n : ℤ) (s : α) (x : E), (↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x

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

Defined in

Mathlib.Algebra.Module.Basic

Cited by

0 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupDivisionRingModuleDistribSMul