[Merged by Bors] - feat(algebra/group/with_one): more API for with_zero

[kbuzzard]

---

I need this to prove that with_zero (multiplicative int) is a linear_ordered_comm_group_with_zero.

[semorrison]

Labelling as WIP while it's not building.

[kbuzzard]

I am being trolled by the linter. This PR is nearly ready except that the linter complained here that with_one.coe_mul wasn't a good simp lemma because it could be proved using with_zero.coe_mul. I am not sure I believe the linter here.

[jcommelin]

@kbuzzard Try proving with_zero.coe_mul using with_one.coe_mul _ _. It works.
But by simp only [with_one.coe_mul] will not prove it.
However, click on the up arrows in the goal state of

@[simp, norm_cast] lemma coe_mul {α : Type u} [has_mul α]
  {a b : α} : ((a * b : α) : with_zero α) = a * b :=
by { simp, /- cursor here -/ }

simp managed to mix with_zero and with_one. This seems bad.

Putting

local attribute [irreducible] with_zero with_one

at the bottom of the file, before the #lint the complaints.
Maybe, if the API is solid, you should mark with_zero and with_one as irreducible.

[kbuzzard]

OK this is ready for review. The main result is that if G is an ordered_comm_monoid then so is with_zero G; the instance was not there. I add some simp lemmas too.

[fpvandoorn]

LGTM, here are some minor suggestions.

[kbuzzard]

Thanks for these @fpvandoorn

[fpvandoorn]

LGTM

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests