English
If E is a vector space over R,S with Rat casting, then for r ∈ ℚ, (r)•x is independent of the choice of base ring.
Русский
Если E — векторное пространство над R, S с наведением Раt, то (r)•x не зависит от выбора кольца-основы.
LaTeX
$$$(r : R) \\cdot x = (r : S) \\cdot x$$$
Lean4
/-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
agree on rational numbers in `R` and `S`. -/
theorem ratCast_smul_eq {E : Type*} (R S : Type*) [AddCommGroup E] [DivisionRing R] [DivisionRing S] [Module R E]
[Module S E] (r : ℚ) (x : E) : (r : R) • x = (r : S) • x :=
map_ratCast_smul (AddMonoidHom.id E) R S r x
