mathlib
23f67f2f - chore(data/rat/cast): split (#17761)

Commit
3 years ago
chore(data/rat/cast): split (#17761) Split off `data/rat/big_operators` from `data/rat/cast`, removing the `algebra/big_operators/basic` import (and, as a consequence, `finset`) from the latter. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Author
Parents
Loading