monoid_hom for units

Stream: Is there code for X?

[Bolton Bailey]

I would like to be able to access the monoid_hom structure for the coercion of units M to M. Does this exist?

[Johan Commelin]

src/algebra/group/units_hom.lean:def coe_hom : units M →* M := ⟨coe, coe_one, coe_mul⟩

[Johan Commelin]

Just search for units.*→[*]. The output isn't too long.

[Bolton Bailey]

Johan Commelin said:

Just search for units.*→[*]. The output isn't too long.

Can you explain what you mean by this?

[Bolton Bailey]

Is this some search technique I can use to find things more easily in the future? Where do I enter that search term?

[Scott Morrison]

Johan is just suggesting you use the search functionality in VSCode. It accepts regular expressions.

[Scott Morrison]

Thus units.*→[*] will find any line in mathlib which contains units, then any string of characters, then →*.

[Scott Morrison]

(He's used the brackets to create a character range, so the last * is literally an asterisk, rather than a regex modifier.)

[Johan Commelin]

@Bolton Bailey https://xkcd.com/208/

[Bolton Bailey]

I see, I am not too familiar with regex, and I didn't recognize the above as a regex with an escaped asterisk. Thanks very much!

[Scott Morrison]

Another potential solution:

import algebra.group.units_hom

example (M : Type) [monoid M] : units M →* M := by library_search

Note that you have to have the right imports open for this to work! But often you're lucky as the relevant file has already been imported because of the definitions you're working with.

[Bolton Bailey]

Indeed, I tried using library_search, but didn't find it that way. I don't think it was because of a missing import though, because hom_coe itself was found just fine. Let me investigate.

[Bolton Bailey]

I think I wrote it without the by actually. My bad.