Theorems · Theorem · commutative algebra

inv_intCast_smul_eq

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

If E is a vector space over two division rings R and S, then scalar multiplications agree on inverses of integer numbers in R and S.

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

AddCommGroupDivisionRingDivisionRingModuleModule