silly bug in division_ring_has_div

Stream: general

[Abhimanyu Pallavi Sudhir]

division_ring_has_div takes two identical instances of division_ring α. Presumably this is a bug.

[Abhimanyu Pallavi Sudhir]

(it's in core, though)

[Patrick Massot]

Such bugs happen

[Patrick Massot]

And if it's in core it will stay there until Lean 4

[Patrick Massot]

Please don't open an issue or submit a PR fixing it, it wouldn't do any good.

[Simon Hudon]

Actually, I think we could take such issues on the leanprover-community fork

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir I would recommend just writing division_ring_has_div' and hoping that division_ring_has_div isn't used in too many other places in lean or mathlib :-)

[Kevin Buzzard]

Oh it's even an instance! So you'd better make another instance with higher priority :-)

[Johan Commelin]

It seems that it isn't used in mathlib so far

[Abhimanyu Pallavi Sudhir]

Oh it's even an instance! So you'd better make another instance with higher priority :-)

Ah ok.
Wait -- is priority 100 lower or higher than priority 200? Which direction does priority go?

[Johan Commelin]

Higher priority is higher

[Kevin Buzzard]

It seems that it isn't used in mathlib so far

division_ring_has_div doesn't appear in core other than that one occurrence -- but because it's an instance it might be used in other places.

[Keeley Hoek]

@Abhimanyu Pallavi Sudhir and the default priority is 1000