English
For any E with two division rings R and S acting linearly, inverses of natural numbers act the same via R and S on smul.
Русский
Для E с двумя кольцами деления R и S скалярное действие по обратным натуральным числам согласуется между R и S.
LaTeX
$$$ (n)^{-1} \cdot x = (n)^{-1} \cdot x $$$
Lean4
/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
agree on inverses of natural numbers in `R` and `S`. -/
theorem inv_natCast_smul_eq {E : Type*} (R S : Type*) [AddCommMonoid E] [DivisionSemiring R] [DivisionSemiring S]
[Module R E] [Module S E] (n : ℕ) (x : E) : (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
map_inv_natCast_smul (AddMonoidHom.id E) R S n x
