English
An identity map preserves the equality f((z⁻¹)•x) = (z⁻¹)•f(x) for z ∈ ℤ via different casts.
Русский
Отображение сохраняет равенство f((z⁻¹)•x) = (z⁻¹)•f(x) для z ∈ ℤ при различных отображениях.
LaTeX
$$$ f((z^{-1}) \cdot x) = (z^{-1}) \cdot f(x) $$$
Lean4
theorem map_inv_intCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
(f : F) (R S : Type*) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (z : ℤ) (x : M) :
f ((z⁻¹ : R) • x) = (z⁻¹ : S) • f x :=
by
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
· rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]
· simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg, map_inv_natCast_smul _ R S]
