Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC