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.