Cast of nat.choose

Stream: general

[Yaël Dillies]

data.nat.choose.dvd proves many properties of the cast of nat.choose to... ℚ. Does anyone mind if I generalize?

[Floris van Doorn]

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]

Okay great! Down the rabbit hole I go...

[Yaël Dillies]

But for other cast lemmas, the type is always left implicit, right?

[Floris van Doorn]

That sounds right. I take it back, you probably want the type implicit.

[Anatole Dedecker]

Funny to see this since I'm going to need this very soon too :smile:

[Kevin Buzzard]

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]

Nice to know it'll be useful beyond me!