Unit lemmas

Stream: general

[Yaël Dillies]

Why is there no lemma of the form u * u^-1 = 1, (a * u^-1) * u, etc... where is_unit u? All I can find is lemmas about \u u where u : units \a.

[Junyan Xu]

Can you even write u^-1? The type of u doesn't necessarily has_inv.

[Yaël Dillies]

I gather that currently the only time we have a pseudo-inverse is with group_with_zero and matrix (and the latter rather uses docs#ring.inverse), but this will change after #13860.

[Yaël Dillies]

My use case is that {u} : set \a is a unit when u is, and additive combinatorics uses that fact all over the place.

[Junyan Xu]

but we do have docs#is_unit.coe_inv_mul

[Yaël Dillies]

Yes exactly. This is about the coercion of the inverse of the unit corresponding to u, rather than the inverse of u itself

[Yaël Dillies]

My use case is precisely when my type already has an inverse, so that I don't have to resort to calculations in the units.

[Junyan Xu]

In group_with_zero (in particular field) the inverse isn't well behaved though, because 0 * 0^-1 is not 0.

[Yaël Dillies]

... which is why you assume is_unit u and call ^-1 a pseudo-inverse

[Eric Wieser]

Is docs#ring.inverse_mul_cancel what you're looking for?

[Yaël Dillies]

Yes! except that I want the ^-1 spelling because ring.inverse does not behave well for additive combinatorics.

[Junyan Xu]

docs#group_with_zero.mul_inv_cancel has the form you require.

[Yaël Dillies]

Yes, except that set \a is not a group_with_zero so it doesn't apply.

[Eric Wieser]

Your question doesn't make sense because there is no typeclass that forces has_inv to mean anything in the context that isn't group_with_zero

[Yaël Dillies]

Yes but #13860 changes this

[Yaël Dillies]

Sorry I shouldn't have asked a question I knew the answer to :stuck_out_tongue:

[Eric Wieser]

Well then your answer to "why is there no lemma of the form ..." is "because such a lemma would require a generalization elsewhere"

[Yaël Dillies]

I believe that what I can do is take the group_with_zero lemmas, and generalize them to my new division_monoid by changing a \ne 0 with is_unit a.

[Eric Wieser]

We already do have the lemmas for the spellings that are possible today; I assume there's one for matrix.has_inv too

[Yaël Dillies]

I wanted to make sure there was no other reason.

[Yaël Dillies]

I believe that what I can do is take the group_with_zero lemmas, and generalize them to my new division_monoid by changing a \ne 0 with is_unit a.

Would you be happy if I were to actually replace the group_with_zero lemmas and add a very easy way to convert a \ne 0 into is_unit a (something like ne.is_unit)?

[Eric Wieser]

That just sounds annoying

[Eric Wieser]

I'd put the new lemmas you're describing in the is_unit namespace

[Yaël Dillies]

This might even be an improvement because dot notation will make that seamless: h.is_unit.the_generalized_lemma

[Eric Wieser]

In my experience you don't normally have h lying around, and it's more convenient to let lean work out you need it after a rewrite

[Eric Wieser]

So dot notation isn't going to be relevant

[Yaël Dillies]

Eh okay, I have a different experience.

[Eric Wieser]

At any rate, it will quickly become annoying to provide is_unit obligations when working in a group

[Eric Wieser]

If you have convenience wrappers for the group lemmas, then let's just have them for group_with_zero too