Topic: norm_cast changes?
Eric Rodriguez (Apr 27 2022 at 11:32):
norm_cast's behaviour has changed a lot in flt-regular, and I can't seem to find any PRs that mention this on the RSS from a quick ctrl+f - is this intended? some of the suggestions it makes are odd, too... for example:
↑⟨x, hx⟩ = (-1) ^ ↑k * ↑↑(zeta_unit' p) ^ m ->
x = ↑(int.neg_of_nat 1 ^ ↑k) * ↑↑(zeta_unit' p ^ m) (and the multiplications are compatible, so I'm not sure why it doesn't coalesce them together as before)
Eric Wieser (Apr 27 2022 at 20:51):
What types are the coercions?
Eric Rodriguez (Apr 27 2022 at 21:48):
Inner one is units, second one is subalgebra (we're dealing with elements of O (Q(zeta)) here)
Last updated: Aug 03 2023 at 10:10 UTC