homogenization.lean

Stream: FLT-regular

[Riccardo Brasca]

The decidable_classical Linter is quite unhappy about src/ring_theory/polynomial/homogenization.lean... I've added some @[nolint decidable_classical] to keep the green sign on GitHub, but sooner or later we will have to fix these.

[Alex J. Best]

Yeah I don't know how to fix them unfortunately

[Alex J. Best]

Adding nolint make sense in that case though, thanks

[Riccardo Brasca]

It's fixed now, without all the nolint.

[Riccardo Brasca]

I am not sure it is the best way of doing this, but you can see all the change in commit c813f0f.

[Alex J. Best]

Oh nice thanks, yeah that looks good, tbh I didn't realise I still had open locale classical in the file

[David Ang]

Hello, are there any plans to PR large chunks of this file into mathlib (or should the “correct” definition of homogenisation in mathlib be more general?)? I’m not part of this project, but I need this for something else, and I’m happy to help out with the golfing or documentation etc if necessary!

[Riccardo Brasca]

cc @Alex J. Best that I think wrote it

[Alex J. Best]

There are plans in my head to PR it but i don't have a lot of time for that right now (but I'd like to do so within a month let's say), i think the definitions are good and don't necessarily need changing for mathlib. Do you need it for something you are PRing to mathlib very soon? Feel free to use it of course, and to make contributions!

[David Ang]

Sounds good! It’s not urgent at all

[Riccardo Brasca]

The decidable_classical Linter is quite unhappy about src/ring_theory/polynomial/homogenization.lean... I've added some @[nolint decidable_classical] to keep the green sign on GitHub, but sooner or later we will have to fix these.

[Alex J. Best]

Yeah I don't know how to fix them unfortunately

[Alex J. Best]

Adding nolint make sense in that case though, thanks

[Riccardo Brasca]

It's fixed now, without all the nolint.

[Riccardo Brasca]

I am not sure it is the best way of doing this, but you can see all the change in commit c813f0f.

[Alex J. Best]

Oh nice thanks, yeah that looks good, tbh I didn't realise I still had open locale classical in the file

[David Ang]

Hello, are there any plans to PR large chunks of this file into mathlib (or should the “correct” definition of homogenisation in mathlib be more general?)? I’m not part of this project, but I need this for something else, and I’m happy to help out with the golfing or documentation etc if necessary!

[Riccardo Brasca]

cc @Alex J. Best that I think wrote it

[Alex J. Best]

There are plans in my head to PR it but i don't have a lot of time for that right now (but I'd like to do so within a month let's say), i think the definitions are good and don't necessarily need changing for mathlib. Do you need it for something you are PRing to mathlib very soon? Feel free to use it of course, and to make contributions!

[David Ang]

Sounds good! It’s not urgent at all

[Riccardo Brasca]

@David Ang are you still interested in having homogenization in mathlib? I think @Yaël Dillies was also interested at some point.

[Riccardo Brasca]

I would like to start again PRing stuff from flt-regular to mathlib, so feel free to take whatever you want!

[David Ang]

I'm happy to have it in mathlib, but at the moment I don't need it immediately.

[Yaël Dillies]

I said I would do it, but haven't had time yet. Maybe in two weeks?

[Ruben Van de Velde]

You don't have enough to do? :)

[Riccardo Brasca]

No pressure at all!

[Riccardo Brasca]

I would start with something else anyway

[Yaël Dillies]

Eh, I'm going to work on Lean full time for six weeks (thanks Kalle :pray:), so I better get a somewhat long todo list :stuck_out_tongue_closed_eyes:

[Michael Stoll]

Will you get to do the order/algebra refactor? :innocent:

[Yaël Dillies]

Hopefully :fingers_crossed:

[Riccardo Brasca]

@Yaël Dillies are you still interested in doing this?

[Yaël Dillies]

Yes, although if I don't get it done next week you can safely assume I've dropped the ball