English
In a vector space over two division rings, inverses of integers act identically via the two scalar structures.
Русский
Вектора пространства над двумя кольцами деления, обратные целые числа действуют одинаково в обеих структурах умножения.
LaTeX
$$$ (n)^{-1} \cdot x = (n)^{-1} \cdot x $$$
Lean4
/-- 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`. -/
theorem inv_intCast_smul_eq {E : Type*} (R S : Type*) [AddCommGroup E] [DivisionRing R] [DivisionRing S] [Module R E]
[Module S E] (n : ℤ) (x : E) : (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
map_inv_intCast_smul (AddMonoidHom.id E) R S n x
