injective + mul bundling

Stream: Is there code for X?

[Damiano Testa]

Dear All,

the two lemmas below assume that there is a multiplicative, injective homomorphism between two types. As you can see, one bundles injectivity in the map and assumes separately that the map respects products. The other does the symmetric choice of bundling multiplication and assuming injectivity.

Is there a full bundling? If not, is one of the two forms below preferable? Or should I unbundle all the way?

Thanks!

variables {G : Type u_1} {H : Type u_2} {B A : finset G} {b0 a0 : G} [has_mul G] [has_mul H]

--  bundles multiplicativity
lemma mul_hom_image_iff [decidable_eq H] (f : G →ₙ* H) (hf : function.injective f) :
  unique_mul (A.image f) (B.image f) (f a0) (f b0) ↔ unique_mul A B a0 b0 :=

--  bundles injectivity
lemma mul_hom_map_iff (f : G ↪ H) (mul : ∀ x y, f (x * y) = f x * f y) :
  unique_mul (A.map f) (B.map f) (f a0) (f b0) ↔ unique_mul A B a0 b0 :=

[Eric Wieser]

I think the first one is more common

[Damiano Testa]

Ok and would it make sense to use map in the first one by passing \<f, hf\> and remove the decidable assumption, or should I simply accept unbundling for injectivity?

[Yaël Dillies]

Probably accept unbundling for injectivity.