units_smul_resolvent_self — Mathlib

English

Let r ∈ Rˣ and a ∈ A. Then r • resolvent(a, r) = resolvent(r⁻¹•a, 1).

Русский

Пусть r ∈ Rˣ, a ∈ A. Тогда r • resolvent(a, r) = resolvent(r⁻¹•a, 1).

LaTeX

$$$r \cdot \operatorname{resolvent}(a, r) = \operatorname{resolvent}(r^{-1}\cdot a, 1)$$$

Lean4

theorem units_smul_resolvent_self {r : Rˣ} {a : A} : r • resolvent a (r : R) = resolvent (r⁻¹ • a) (1 : R) := by
  simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using @units_smul_resolvent _ _ _ _ _ r r a

Похожие утверждения