document the ordering on R[i] (complex.lec and complexltc) #75
Description
A partial order on R[i] is defined in complex.v but undocumented.
This ordering is a bit weird and would need documentation.
@CohenCyril
{{ message }}
A partial order on R[i] is defined in complex.v but undocumented.
This ordering is a bit weird and would need documentation.
@CohenCyril