Lemmas vs‌ Defs

Stream: mathlib4

[Jireh Loreaux]

Can someone please explain to me why Algebra.Order.Ring.Defs imports Algebra.Order.Ring.Lemmas and not the other way around? (aside from "because the decls in the latter are needed in the former", which is obvious)

This totally violates any sort of intuition and the other instances of files with this naming convention in the library.

[Yuyang Zhao]

!3#16520 (algebra.order.monoid_lemmas_zero_lt -> algebra.order.ring_lemmas)
!3#17381 (algebra.order.ring_lemmas -> algebra.order.ring.lemmas)

[Kim Morrison]

I like Std's approach here, which is that if you need a handful of lemmas before you can even get off the ground with the basic definitions, you put those in an Init folder, e.g. moving Algebra.Order.Ring.Lemmas to Algebra.Order.Ring.Init.Lemmas.

Of course, in Mathlib this risks someone thinking these are lemmas about the initial ordered ring. :-)

[Yaël Dillies]

This is not what's happening

[Yaël Dillies]

• "ordered ring" as in Algebra.Order.Ring.Defs -> addition, multiplication, order, all compatible with each other
• Algebra.Order.Ring.Lemmas -> zero, multiplication, order, all compatible with each other

[Yaël Dillies]

I knew this would be confusing when I did the move, but it was semantically definitely better than before and I didn't want to create an Algebra.Order.MonoidWithZero folder for a single file

[Yaël Dillies]

but in fact @Newell Jensen is now migrating more results there, so it might be worth reconsidering

[Kim Morrison]

But
Yaël Dillies said:

• Algebra.Order.Ring.Lemmas -> zero, multiplication, order, all compatible with each other

is surely the wrong name for such a file? It seems to have little to do with the contents.

[Yaël Dillies]

Compare with file#Algebra/Order/Monoid/Lemmas

[Jireh Loreaux]

Right, so why not just Algebra.Order.MonoidWithZero ?