Commit 2025-07-03 05:16 d76db180
View on Github →refactor(Data/NNRat/BigOperators): generalize coe big operator lemmas (#26480)
This refactor generalizes the norm_cast lemmas for sums and products of coercion of ℚ≥0 elements.
Previously, these lemmas were stated only for coercion to ℚ. This change generalizes the target type β to any [DivisionSemiring β] with [CharZero β] for sums, and any [Semifield β] with [CharZero β] for products.