Nuprl - IteratedBinops LEMMAs for iter_prod_zero_iff_factor

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
6	Thm* ( i:{a..b}. e(i)) = 0 (i:{a..b}. e(i) = 0)	[iter_prod_zero_iff_factor_zero]
cites the following:
2	Thm* a,b:, P:({a..b}Prop). (i:{a..b}. P(i)) (Or i:{a..b}. P(i))	[exist_intseg_vs_iter_or]
0	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* ba (Iter(f;u) i:{a..b}. e(i)) = u	[iter_via_intseg_null]
1	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* a<b Thm* Thm* (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1))	[iter_via_intseg_split_last]
5	Thm* a,b:. ab = 0 a = 0 b = 0	[prod_zero_iff_factor_zero]
1	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* ba (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{a..a}. e(i))	[iter_via_intseg_nullnorm]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html