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.

Estimated changes

added theorem NNRat.cast_listProd
added theorem NNRat.cast_listSum
added theorem NNRat.cast_multisetSum
added theorem NNRat.cast_prod
added theorem NNRat.cast_sum
deleted theorem NNRat.coe_list_prod
deleted theorem NNRat.coe_list_sum
deleted theorem NNRat.coe_multiset_prod
deleted theorem NNRat.coe_multiset_sum
deleted theorem NNRat.coe_prod
deleted theorem NNRat.coe_sum