English
If G and H each have UniqueProds, then G × H has UniqueProds.
Русский
Если у G и H есть UniqueProds, то у их произведения G × H есть UniqueProds.
LaTeX
$$$ [\\mathrm{UniqueProds} G][\\mathrm{UniqueProds} H] \\Rightarrow \\mathrm{UniqueProds}(G \\times H). $$$
Lean4
@[to_additive]
instance _root_.Prod.instUniqueProds [UniqueProds G] [UniqueProds H] : UniqueProds (G × H) :=
by
have : ∀ b, UniqueProds (I G H b) := Bool.rec ?_ ?_
· exact of_injective_mulHom (downMulHom H) down_injective ‹_›
· refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he => Prod.ext ?_ ?_) (UniqueProds.instForall <| I G H) <;>
apply up_injective
exacts [congr_fun he false, congr_fun he true]
· exact of_injective_mulHom (downMulHom G) down_injective ‹_›
