English
UniqueMul is preserved under inverse images along an injective multiplicative map.
Русский
UniqueMul сохраняется под обратными образами вдоль инъективного мультипликативного отображения.
LaTeX
$$$\\text{UniqueMul}(A,B,a_0,b_0) \\Rightarrow \\text{UniqueMul}(A^{\\mathrm{preimage}}_{f}, B^{\\mathrm{preimage}}_{f}, a_0, b_0)$ for an injective f$$
Lean4
/-- `UniqueMul` is preserved by inverse images under injective, multiplicative maps. -/
@[to_additive /-- `UniqueAdd` is preserved by inverse images under injective, additive maps. -/
]
theorem mulHom_preimage (f : G →ₙ* H) (hf : Function.Injective f) (a0 b0 : G) {A B : Finset H}
(u : UniqueMul A B (f a0) (f b0)) : UniqueMul (A.preimage f hf.injOn) (B.preimage f hf.injOn) a0 b0 :=
by
intro a b ha hb ab
simp only [← hf.eq_iff, map_mul] at ab ⊢
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab
