English
Let r be a unit in R and s ∈ R. For any a ∈ A, r acting on the resolvent at s equals the resolvent at r⁻¹•a and r⁻¹•s: r • resolvent(a,s) = resolvent(r⁻¹•a, r⁻¹•s).
Русский
Пусть r — единица в R и s ∈ R. Тогда действие единицы на резольвенту даёт: r⁻¹•a и r⁻¹•s; формула: r • Resolvent(a,s) = Resolvent(r⁻¹•a, r⁻¹•s).
LaTeX
$$$r \in R^{\times},\; s \in R:\; r \cdot \operatorname{resolvent}(a,s) = \operatorname{resolvent}(r^{-1}\cdot a, r^{-1}\cdot s)$$$
Lean4
theorem units_smul_resolvent {r : Rˣ} {s : R} {a : A} : r • resolvent a (s : R) = resolvent (r⁻¹ • a) (r⁻¹ • s : R) :=
by
by_cases h : s ∈ spectrum R a
· rw [mem_iff] at h
simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
rw [smul_assoc, ← smul_sub]
have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu => h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]
· simp only [resolvent]
have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using notMem_iff.mp h
rw [← h'.val_subInvSMul, ← (notMem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit, h'.val_inv_subInvSMul]
simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]
