---

Step * of Lemma real-Cramers-rule

∀[n:ℕ]. ∀[A:ℝ(n × n)].  ∀[b:ℝ^n]. (A*col(λj.(|λx,y. if y=j then b x else (A x y)|/|A|))) ≡ col(b) supposing |A| ≠ r0
BY
{ (Auto
   THEN (InstLemma `real-Cramers-rule1` [⌜n⌝;⌜A⌝;⌜(r1/|A|)⌝;⌜b⌝]⋅ THENA Auto)
   THEN (RWO "-1<" 0 THENM BLemma `real-matrix-times_functionality`)
   THEN Auto
   THEN Try ((RelRST THEN Auto))) }

1
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)|)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbR{}(n  \mtimes{}  n)].
    \mforall{}[b:\mBbbR{}\^{}n].  (A*col(\mlambda{}j.(|\mlambda{}x,y.  if  y=j  then  b  x  else  (A  x  y)|/|A|)))  \mequiv{}  col(b)  supposing  |A|  \mneq{}  r0


By

---

Latex:
(Auto
  THEN  (InstLemma  `real-Cramers-rule1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}(r1/|A|)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENM  BLemma  `real-matrix-times\_functionality`)
  THEN  Auto
  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index