Eliminating `algebra {ℕ,ℤ,ℚ} R` diamonds

Stream: general

[Anne Baanen]

I have been getting annoyed by the diamonds you get with docs#algebra_nat, docs#algebra_int and docs#algebra_rat versus e.g. docs#algebra.id. The correct solution is to use forgetful inheritance to define the algebra_{nat,int,rat} instances: the to_fun and smul fields in algebra_nat should be set using the [semiring R] instance being passed in; an analogous statement should hold for algebra_int and algebra_rat. More specifically,

• a semiring R instance should contain of_nat : ℕ → R in addition to the nsmul field
• a ring R instance should contain of_int : ℤ → R in addition to the zsmul field
• the combination of division_ring R and char_zero R should contain of_rat : ℚ → R and qsmul : ℚ → R → R

First issue: it's not totally trivial where of_rat should come from, since the current algebra_rat definition takes two instance params. I suppose putting it in division_ring works well enough.

Second issue: if we redefine the algebra instances, should we also redefine the docs#nat.cast_coe, docs#int.cast_coe and docs#rat.cast_coe instances? In particular, the current state of defeq is @@algebra_map _ some_other_algebra ℕ R ≠ @@algebra_map _ algebra_nat ℕ R 0 = ↑0 = 0, should we move the non-defeq one or two steps to the right? Similar for ℤ and ℚ.

Assuming we also redefine docs#nat.cast_coe, where should of_nat actually live, since cast_coe currently requires only notation ([has_zero α] [has_one α] [has_add α]) and no proofs? Similar for ℤ. For ℚ, docs#rat.cast_coe takes a division_ring as parameter so it works fine if we put of_rat in division_ring.

[Anne Baanen]

And restricting the coercion from ℕ to only (non-assoc) semirings isn't going to work, since docs#with_top currently has a coercion from ℕ but isn't a semiring.

[Eric Rodriguez]

I think @Gabriel Ebner was working on a solution for of_nat with add_monoid_with_one, but I'm not sure where the PR is

[Eric Rodriguez]

it's a pretty big one IIRC

[Anne Baanen]

For the moment I'll concentrate on the ℚ algebra diamond only, since I don't see any big obstacles at this moment.

[Eric Wieser]

Note that #12182 already adds of_nat and of_int (edit: that's the PR @Eric Rodriguez is referring to)

[Anne Baanen]

I created the PR series fixing the ℚ algebra diamond (once I've resolved any build errors). First a set of PRs for readjusting the import hierarchy:

• #14849
• #14890

• #14893
  And the PR redefining algebra_rat to make use of new of_rat and qsmul fields in division_ring

• #14894