add_div not as general as it should be?

Stream: new members

[Daniele Pusceddu]

Hello, I wanted to use add_div with my positive reals subtype and was surprised that I couldn't because it requires a DivisionSemiring instance.
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Field/Basic.html#add_div

I had to write my own version that uses only DivInvMonoid and RightDistribClass.

theorem add_div'' {α: Type}
[DivInvMonoid α] [Add α] [RightDistribClass α]
(a b c: α):
(a + b) / c = a/c + b/c :=
  by simp_rw [div_eq_mul_inv, add_mul]

Is there any reason for this that I'm missing?
Disclaimer: I am terrible at math so sorry if I'm saying something stupid.

[Eric Wieser]

docs#right_distrib_class is fairly new, so I think we just didn't notice this generalization becoming available

[Daniele Pusceddu]

Eric Wieser said:

docs#right_distrib_class is fairly new, so I think we just didn't notice this generalization becoming available

Since I would like this generalization for myself, would it be too difficult for me to contribute it to mathlib, having no previous experience? I assume there will be other theorems requiring the same generalization for consistency

[Eric Wieser]

Ideally you would either:

• Contribute the generalization to mathlib3, then forward port it
• Wait for the port from mathlib3 to mathlib4 to be complete, then contribute it in mathlib4

[Jireh Loreaux]

Eric, given that this is just a type class generalization, is there any reason not to contribute directly to mathlib4?

[Eric Wieser]

Generalizations can sometimes cause unification problems downstream. It also stops someone generalizing the mathlib3 results in a different direction somehow

[Eric Wieser]

We had a case recently where things were added to mathlib4 and then conflicted with bits of mathlib3 that hadn't been ported yet

[Daniele Pusceddu]

Eric Wieser said:

Ideally you would either:

• Contribute the generalization to mathlib3, then forward port it
• Wait for the port from mathlib3 to mathlib4 to be complete, then contribute it in mathlib4

I'd have to opt for the second option since I have never even touched Lean3 and I believe that would be too much work for me right now sadly.

[Kevin Buzzard]

You could start working on the PR now and then it could be reviewed when people are confident that it won't cause problems with the port. In two weeks' time the port might be all over bar the shouting anyway