Topic: Cast of nat.choose
Yaël Dillies (Aug 01 2021 at 14:46):
data.nat.choose.dvd proves many properties of the cast of
ℚ. Does anyone mind if I generalize?
Floris van Doorn (Aug 01 2021 at 14:48):
Generalizing to arbitrary fields sounds great!
You should probably make the field explicit if it cannot be figured out from other assumptions.
Yaël Dillies (Aug 01 2021 at 14:48):
Okay great! Down the rabbit hole I go...
Yaël Dillies (Aug 01 2021 at 14:49):
But for other cast lemmas, the type is always left implicit, right?
Floris van Doorn (Aug 01 2021 at 14:55):
That sounds right. I take it back, you probably want the type implicit.
Anatole Dedecker (Aug 01 2021 at 19:10):
Funny to see this since I'm going to need this very soon too :smile:
Kevin Buzzard (Aug 01 2021 at 19:11):
It's great when that happens isn't it! In fact it happens a lot more often than you think -- sometimes you use stuff and have no idea it was PRed two weeks ago.
Yaël Dillies (Aug 01 2021 at 19:24):
Nice to know it'll be useful beyond me!
Last updated: Aug 03 2023 at 10:10 UTC