Zulip Chat Archive

Stream: mathlib4

Topic: algebra.euclidean_domain.instances

Chris Hughes (Dec 27 2022 at 15:32):

This is ported but not marked as such on the port status page

Anatole Dedecker (Dec 28 2022 at 19:33):

And that's not just visual, because algebra.order.euclidean_absolute_value is ready to port but not listed as so because of this one

Reid Barton (Dec 28 2022 at 19:42):

Its source header is missing the word module

! This file was ported from Lean 3 source algebra.euclidean_domain.instances

Reid Barton (Dec 28 2022 at 19:43):

mathlib4#1249

Reid Barton (Dec 28 2022 at 19:46):

Found one other one, mathlib4#1250

Reid Barton (Dec 28 2022 at 19:47):

I'm just going to merge these fixes.

Last updated: Dec 20 2023 at 11:08 UTC