mathlib3
d75314b3
- fix(data/nat/interval): do not dedup when implementing `finset.Icc` etc (#16423)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(data/nat/interval): do not dedup when implementing `finset.Icc` etc (#16423) This means that `finset.Iic n` no longer has quadratic complexity. `#eval (finset.Iic 200000).card` is now almost instant rather than taking a very long time.
Author
eric-wieser
Parents
370dabe7
Loading