English
Uniqueness is preserved under maps that are multiplicative embeddings; mapping via an embedding f preserves the UniqueMul property.
Русский
Уникальность сохраняется под отображениями, которые являются вложениями, и через отображение f сохраняется свойство UniqueMul.
LaTeX
$$UniqueMul (A.map f) (B.map f) (f a0) (f b0) ↔ UniqueMul A B a0 b0 for f : G ↪ H with multiplicative structure$$
Lean4
/-- `Unique_Mul` is preserved under multiplicative maps that are injective.
See `UniqueMul.mulHom_map_iff` for a version with swapped bundling. -/
@[to_additive /-- `UniqueAdd` is preserved under additive maps that are injective.
See `UniqueAdd.addHom_map_iff` for a version with swapped bundling. -/
]
theorem mulHom_image_iff [DecidableEq H] (f : G →ₙ* H) (hf : Function.Injective f) :
UniqueMul (A.image f) (B.image f) (f a0) (f b0) ↔ UniqueMul A B a0 b0 :=
⟨of_mulHom_image f fun _ _ _ _ _ ↦ .imp (hf ·) (hf ·), fun h _ _ ↦
by
simp_rw [Finset.mem_image]
rintro ⟨a, aA, rfl⟩ ⟨b, bB, rfl⟩ ab
simp_rw [← map_mul, hf.eq_iff] at ab ⊢
exact h aA bB ab⟩
