of_mulHom_image — Mathlib

English

UniqueMul is preserved under injective multiplicative maps when passing to image sets.

Русский

UniqueMul сохраняется под инъективными мультипликативными отображениями при переходе к образам.

LaTeX

$$UniqueMul (A.image f) (B.image f) (f a0) (f b0) ↔ UniqueMul A B a0 b0 for an injective f$$

Lean4

@[to_additive]
theorem of_mulHom_image [DecidableEq H] (f : G →ₙ* H)
    (hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d)
    (h : UniqueMul (A.image f) (B.image f) (f a0) (f b0)) : UniqueMul A B a0 b0 := fun a b ha hb ab ↦
  hf ab (h (Finset.mem_image_of_mem f ha) (Finset.mem_image_of_mem f hb) <| by simp_rw [← map_mul, ab])

Похожие утверждения