English
If E is a vector space over two division semirings R and S, then scalar multiplications agree on nonnegative rationals: for r ∈ ℚ≥0, (r)•x computed via R or via S gives the same result.
Русский
Если E является векторным пространством над двумя делимыми полями R и S, то скаляры из ℚ≥0 совпадают: (r)•x по R равен (r)•x по S.
LaTeX
$$$(r : R) \\cdot x = (r : S) \\cdot x$$$
Lean4
/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
agree on non-negative rational numbers in `R` and `S`. -/
theorem nnratCast_smul_eq {E : Type*} (R S : Type*) [AddCommMonoid E] [DivisionSemiring R] [DivisionSemiring S]
[Module R E] [Module S E] (r : ℚ≥0) (x : E) : (r : R) • x = (r : S) • x :=
map_nnratCast_smul (AddMonoidHom.id E) R S r x
