a,b:
, e:({a..b
}
), i:{a..b}. e(i) | (
i:{a..b}. e(i))a,c,b:, e:({a..b}).
Thm* a
c
Thm*
Thm* c<b
Thm*
Thm* (
i:{a..b}. e(i)) = ( i:{a..c}. e(i))
e(c)( i:{c+1..b}. e(i))| Rank | Theorem | Name |
| 5 | a,b:, e:({a..b}), i:{a..b}. e(i) | ( i:{a..b}. e(i)) | [components_divide_iter_mul] |
| cites the following: | ||
| 4 | a,c,b:, e:({a..b}).
Thm* a c
Thm*
Thm* c<b Thm*
Thm* ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i)) | [mul_via_intseg_split_pluck] |