Theorem NNRat.coe_prod
Modification history
2025-07-03 05:16
Mathlib/Data/NNRat/BigOperators.lean
refactor(Data/NNRat/BigOperators): generalize `coe` big operator lemmas (#26480) …
Deleted NNRat.coe_prodView on Github →2024-05-27 08:32
Mathlib/Data/NNRat/BigOperators.lean
chore: Use the new `∑ i ∈ s, f i` notation (#13209) …
Modified NNRat.coe_prodView on Github →