English
More general preservation: an injective multiplicative homomorphism maps between finite sets A,B and their images preserve UniqueMul equivalence with a0,b0.
Русский
Более общая сохранность: инъективный мультипликативный гомоморфизм сохраняет равенство UniqueMul между A,B и их образами.
LaTeX
$$UniqueMul (Finset.image (MulHom.funLike.coe f) A) (Finset.image (MulHom.funLike.coe f) B) (MulHom.funLike.coe f a0) (MulHom.funLike.coe f b0) ↔ UniqueMul A B a0 b0$$
Lean4
/-- `UniqueMul` is preserved under embeddings that are multiplicative.
See `UniqueMul.mulHom_image_iff` for a version with swapped bundling. -/
@[to_additive /-- `UniqueAdd` is preserved under embeddings that are additive.
See `UniqueAdd.addHom_image_iff` for a version with swapped bundling. -/
]
theorem mulHom_map_iff (f : G ↪ H) (mul : ∀ x y, f (x * y) = f x * f y) :
UniqueMul (A.map f) (B.map f) (f a0) (f b0) ↔ UniqueMul A B a0 b0 := by
classical simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]; rfl
