mathlib3
9d931dbd - chore(analysis/specific_limits/basic): generalize away from `ℝ`

Commit
2 years ago
chore(analysis/specific_limits/basic): generalize away from `ℝ` In practice the only difference is that this now supports `ℚ`
Author
Parents
Loading