---

Step * 1 of Lemma matrix-ring_wf


1. r : Rng
2. n : ℕ
⊢ matrix-ring(r;n) ∈ RngSig
BY
{ (RepUR ``matrix-ring rng_sig`` 0 THEN MemCD THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  n  :  \mBbbN{}
\mvdash{}  matrix-ring(r;n)  \mmember{}  RngSig


By

---

Latex:
(RepUR  ``matrix-ring  rng\_sig``  0  THEN  MemCD  THEN  Auto)

---

Home Index