Step * 1 of Lemma quot_ring_car_subtype

.....subterm..... T:t
1:n
1. CRng
2. Ideal(r){i}
3. ∀x:|r|. SqStable(a x)@i
4. detach_fun(|r|;a)
5. |r|@i
⊢ x ∈ Carrier(r/d)
BY
Unfold `quot_ring_car` 0⋅ }

1
1. CRng
2. Ideal(r){i}
3. ∀x:|r|. SqStable(a x)@i
4. detach_fun(|r|;a)
5. |r|@i
⊢ x ∈ x,y:|r|//(↑(d (x +r (-r y))))


Latex:


Latex:
.....subterm.....  T:t
1:n
1.  r  :  CRng
2.  a  :  Ideal(r)\{i\}
3.  \mforall{}x:|r|.  SqStable(a  x)@i
4.  d  :  detach\_fun(|r|;a)
5.  x  :  |r|@i
\mvdash{}  x  \mmember{}  Carrier(r/d)


By


Latex:
Unfold  `quot\_ring\_car`  0\mcdot{}




Home Index