Turn a Weil divisor or a Q divisor into a real divisor (or do nothing to a real divisor).
i1 : R = ZZ/5[x]; |
i2 : D = divisor(x) o2 = 1*Div(x) of R o2 : WDiv |
i3 : E = (2/2)*D o3 = 1*Div(x) of R o3 : QDiv |
i4 : F = toRDiv(E) o4 = 1*Div(x) of R o4 : RDiv |
i5 : G = toRDiv(D) o5 = 1*Div(x) of R o5 : RDiv |
i6 : F == G o6 = true |