unit_smul_eq_smul — Mathlib

English

Let r ∈ Units R, s ∈ R, a ∈ A. Then r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s).

Русский

Пусть r ∈ единицы R, s ∈ R, a ∈ A. Тогда r • резольвента(a,s) = резольвента (r⁻¹ • a) (r⁻¹ • s).

LaTeX

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

Lean4

theorem unit_smul_eq_smul (a : A) (r : Rˣ) : σ (r • a) = r • σ a :=
  by
  ext x
  have x_eq : x = r • r⁻¹ • x := by simp
  nth_rw 1 [x_eq]
  rw [smul_mem_smul_iff]
  constructor
  · exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
  · rintro ⟨w, _, (x'_eq : r • w = x)⟩
    simpa [← x'_eq]
      -- `r ∈ σ(a*b) ↔ r ∈ σ(b*a)` for any `r : Rˣ`

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