naming of binary properties with left and right

Stream: maths

[Sean Leather]

@Chris Hughes updated his finset.disjoint PR with a change to rename the following:

• empty_disjoint → disjoint_empty_left
• disjoint_empty → disjoint_empty_right

Personally, I prefer the new names: they are more descriptive and don't rely on positional naming, which can be confusing. But I wanted to open up a discussion on this in general to determine the mathlib style guidelines. I don't think these types of things have been consistently named.

[Sean Leather]

We probably want feedback from @Johannes Hölzl and @Mario Carneiro in particular.

[Chris Hughes]

There's also the question of which one's right and which one's left. I would have named dvd_mul_right : a ∣ a * b dvd_mul_left

[Kenny Lau]

@Chris Hughes confer or.inl and or.inr

[Sean Leather]

I created a GitHub issue for this discussion. Please leave any thoughts there.