genEigenspace_div — Mathlib

English

For a, b ∈ K with b ≠ 0, genEigenspace f (a/b) 1 equals ker (b f − a 1).

Русский

Для a, b ∈ K с b ≠ 0, genEigenspace f (a/b) 1 равно ker (b f − a 1).

LaTeX

$$genEigenspace f (a/b) 1 = \ker (b f - a \cdot 1)$$

Lean4

theorem genEigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
    genEigenspace f (a / b) 1 = LinearMap.ker (b • f - a • 1) :=
  calc
    genEigenspace f (a / b) 1 = genEigenspace f (b⁻¹ * a) 1 := by rw [div_eq_mul_inv, mul_comm]
    _ = LinearMap.ker (f - (b⁻¹ * a) • 1) := by rw [genEigenspace_one]
    _ = LinearMap.ker (f - b⁻¹ • a • 1) := by rw [smul_smul]
    _ = LinearMap.ker (b • (f - b⁻¹ • a • 1)) := by rw [LinearMap.ker_smul _ b hb]
    _ = LinearMap.ker (b • f - a • 1) := by rw [smul_sub, smul_inv_smul₀ hb]

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