Description: The dimension of a vector of a module with indices from 0 to N - 1 . (Contributed by SN, 1-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frlmfzowrd.w | ||
frlmfzowrd.b | |||
frlmfzowrd.s | |||
Assertion | frlmfzolen |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frlmfzowrd.w | ||
2 | frlmfzowrd.b | ||
3 | frlmfzowrd.s | ||
4 | ovexd | ||
5 | 1 3 2 | frlmbasf | |
6 | 4 5 | sylan | |
7 | fnfzo0hash | ||
8 | 6 7 | syldan |