Step
*
1
of Lemma
real-Cramers-rule
1. n : ℕ
2. A : ℝ(n × n)
3. |A| ≠ r0
4. b : ℝ^n
5. (A*(r1/|A|)*col(λj.|λx,y. if y=j then b x else (A x y)|)) ≡ col(b)
⊢ col(λj.(|λx,y. if y=j then b x else (A x y)|/|A|)) ≡ (r1/|A|)*col(λj.|λx,y. if y=j then b x else (A x y)|)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN RepUR ``real-matrix-scalar-mul rcolumn`` 0 THEN Auto) }
Latex:
Latex:
1. n : \mBbbN{}
2. A : \mBbbR{}(n \mtimes{} n)
3. |A| \mneq{} r0
4. b : \mBbbR{}\^{}n
5. (A*(r1/|A|)*col(\mlambda{}j.|\mlambda{}x,y. if y=j then b x else (A x y)|)) \mequiv{} col(b)
\mvdash{} col(\mlambda{}j.(|\mlambda{}x,y. if y=j then b x else (A x y)|/|A|)) \mequiv{} (r1/|A|)*col(\mlambda{}j.|\mlambda{}x,y. if y=j
then b x
else (A x y)|)
By
Latex:
(RepeatFor 2 ((D 0 THENA Auto)) THEN RepUR ``real-matrix-scalar-mul rcolumn`` 0 THEN Auto)
Home
Index