`BookProof.ChapterH5.inversion_free_seed` (S R : E →ₗ[K] E) (v₀ : E) (m : ℕ) (hR : R.comp S = LinearMap.id) : R ((S ^ (m + 1)) v₀) = (S ^ m) v₀

Initializing...

`BookProof.ChapterH5.inversion_free_seed` (S R : E →ₗ[K] E) (v₀ : E) (m : ℕ) (hR : R.comp S = LinearMap.id) : R ((S ^ (m + 1)) v₀) = (S ^ m) v₀ · Prove2Me