---

Step * of Lemma matrix-scalar-mul-1

∀[n,m:ℕ]. ∀[r:Rng]. ∀[M:Matrix(n;m;r)].  (1*M = M ∈ Matrix(n;m;r))
BY
{ ((Auto THEN RepUR ``matrix-scalar-mul`` 0 THEN Unfold `matrix` 0 THEN RepeatFor 2 ((FunExt THENA Auto)))
   THEN Fold `matrix-ap` 0
   THEN Reduce 0) }

1
1. n : ℕ
2. m : ℕ
3. r : Rng
4. M : Matrix(n;m;r)
5. x : ℕn
6. x1 : ℕm
⊢ (1 * M[x,x1]) = M[x,x1] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[r:Rng].  \mforall{}[M:Matrix(n;m;r)].    (1*M  =  M)


By

---

Latex:
((Auto
    THEN  RepUR  ``matrix-scalar-mul``  0
    THEN  Unfold  `matrix`  0
    THEN  RepeatFor  2  ((FunExt  THENA  Auto)))
  THEN  Fold  `matrix-ap`  0
  THEN  Reduce  0)

---

Home Index