---

Step * 2 of Lemma matrix-ring_wf

.....set predicate..... 
1. r : Rng
2. n : ℕ
⊢ IsRing(|matrix-ring(r;n)|;+matrix-ring(r;n);0;-matrix-ring(r;n);*;1)
BY
{ (RepUR ``ring_p group_p monoid_p bilinear assoc ident inverse`` 0 THEN SplitAndConcl THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  r  :  Rng
2.  n  :  \mBbbN{}
\mvdash{}  IsRing(|matrix-ring(r;n)|;+matrix-ring(r;n);0;-matrix-ring(r;n);*;1)


By

---

Latex:
(RepUR  ``ring\_p  group\_p  monoid\_p  bilinear  assoc  ident  inverse``  0  THEN  SplitAndConcl  THEN  Auto)

---

Home Index