Zulip Chat Archive

Stream: general

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 nat.choose to... . 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: Dec 20 2023 at 11:08 UTC