norm_cast changes?

Stream: general

[Eric Rodriguez]

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]

What types are the coercions?

[Eric Rodriguez]

Inner one is units, second one is subalgebra (we're dealing with elements of O (Q(zeta)) here)