mulLeftEmbedding for IsLeftCancelMulZero

Stream: Is there code for X?

[shortc1rcuit]

I want to use map on a Finset ℕ to send x to k * x, which needs an embedding rather than just a function. Looking at Mathlib I can see that there is a definition for an embedding of left multiplication, but it's only for types of IsLeftCancelMul, which ℕ isn't. Is there an equivalent definition in Mathlib for IsLeftCancelMulZero?

[Yaël Dillies]

Do you know in your case that k ≠ 0?

[Yaël Dillies]

file#Mathlib/Algebra/Group/Pointwise/Finset/Scalar might be interesting regardless

[Yakov Pechersky]

Do you need to map? Would docs#Finset.image be sufficient?

[shortc1rcuit]

Yaël Dillies said:

Do you know in your case that k ≠ 0?

Yes

Yakov Pechersky said:

Do you need to map? Would docs#Finset.image be sufficient?

Later on in my proof I sum over the finset and I use the theorem Finset.sum_map. So I need to use map as I need to show that no two elements get mapped to the same value.

[shortc1rcuit]

I was able to put together this general definition for what I would like

def mulLeftEmbedding₀ {G : Type u_1} [Mul G] [Zero G] [IsLeftCancelMulZero G] (g : G) (hg : g ≠ 0) : G ↪ G where
  toFun := (g * ·)
  inj' := mul_right_injective₀ hg

[shortc1rcuit]

I'm using this definition in my proof for now, but I'd be interested in maybe adding it to Mathlib if it's not there already.

[Eric Wieser]

I suspect in matlib we tend to just inline this definition

[Yury G. Kudryashov]

Since we have mulLeftEmbedding, it makes sense to have a version for monoids with zero too. I would accept a pr adding it to the library.

[Eric Wieser]

If we add it we should modify the places that currently inline it

[shortc1rcuit]

Yury G. Kudryashov said:

Since we have mulLeftEmbedding, it makes sense to have a version for monoids with zero too. I would accept a pr adding it to the library.

I've not contributed to mathlib before but I'd be interested in doing this. Where should I look to get started?

Also @Eric Wieser what places inline this?

[Eric Wieser]

Searching for all uses of the injectivity lemma should find them