Positive parts

Stream: general

[Yaël Dillies]

@Christopher Hoskin, your docs#lattice_ordered_comm_group.has_one_lattice_has_pos_part is creating a diamond when α is a ring. Then the positive part is both a ⊔ 1 and a ⊔ 0.

[Yaël Dillies]

Not sure this happens in practice, but we should be aware of it.

[Eric Wieser]

Can you elaborate, maybe with an mwe?

[Eric Wieser]

rings aren't commutative groups

[Eric Wieser]

So did you mean docs#lattice_ordered_comm_group.has_zero_lattice_has_pos_part?

[Yaël Dillies]

Ah true. But the instance really only needs the bare syntax typeclasses.

[Yaël Dillies]

So at some point it will get generalized and suddenly a⁺ means two different things.

[Eric Wieser]

It feels like maybe it should have been called has_mul_pos_part

[Eric Wieser]

The pos name seems a pretty weird spelling for "at least 1". Is this from the literature, or just additivized pre-emptively?

[Yaël Dillies]

That we should read from Birkhoff.

[Christopher Hoskin]

In hindsight I should have stuck to my original plan of only developing the theory for additive groups. I'm happy to do a PR to remove the multiplicative case if that would help?

[Christopher Hoskin]

I think this may have been discussed previously, but I don't recall the conclusion.

[Yaël Dillies]

I currently don't see the point of developing the theory of multiplicative groups except that "it can be done". I don't think you need to strip down your work either. We should just have a big warning sign.