Lean checks the proposition indexed as “sum prefix of zero”; the hypotheses and conclusion in the code panel fix its exact scope. Restrict a finite sum to a prefix when all remaining summands vanish.
theorem sum_prefix_of_zero {m n : ℕ} {M : Type*} [AddCommMonoid M]
(hmn : m ≤ n) (f : Fin n → M) (hf : ∀ j, m ≤ j.val → f j = 0) :
(∑ i : Fin m, f (Fin.castLE hmn i)) = ∑ j : Fin n, f j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exists factor of le”; the hypotheses and conclusion in the code panel fix its exact scope. A wide real matrix has an exact factorization with orthonormal rows.
theorem exists_factor_of_le {m n : ℕ} (hmn : m ≤ n)
(A : _root_.Matrix (Fin m) (Fin n) ℝ) :
∃ (R : _root_.Matrix (Fin m) (Fin m) ℝ)
(Q : _root_.Matrix (Fin m) (Fin n) ℝ),
A = R * Q ∧ Q * Q.transpose = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exists thin lq”; the hypotheses and conclusion in the code panel fix its exact scope. Every finite real matrix admits a thin factorization with exactly 'min m n' orthonormal rows.
theorem exists_thin_lq {m n : ℕ} (A : _root_.Matrix (Fin m) (Fin n) ℝ) :
∃ (R : _root_.Matrix (Fin m) (Fin (min m n)) ℝ)
(Q : _root_.Matrix (Fin (min m n)) (Fin n) ℝ),
A = R * Q ∧ Q * Q.transpose = 1 := by
commit-pinned source · Verso Blueprint panel