English
If h1 and h2 are Freiman isomorphisms between A1,B1 and A2,B2, then Prod.map f1 f2 is a Freiman iso between A1×A2 and B1×B2.
Русский
Если h1 и h2 — Фримановые изоморфии между A1,B1 и A2,B2, то Prod.map f1 f2 задаёт Фриманову изоморфию между A1×A2 и B1×B2.
LaTeX
$$$IsMulFreimanIso n A1 B1 f1 \\to IsMulFreimanIso n A2 B2 f2 \\Rightarrow IsMulFreimanIso n (A_1 \\times\\!\\!\\, A_2) (B_1 \\times\\!\\!\\, B_2) (Prod.map f_1 f_2)$$$
Lean4
@[to_additive prodMap]
theorem prodMap (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) :
IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
where
bijOn := h₁.bijOn.prodMap h₂.bijOn
map_prod_eq_map_prod s t hsA htA hs
ht := by
simp only [mem_prod, forall_and, Prod.forall] at hsA htA
simp only [Prod.ext_iff, fst_prod, map_map, Function.comp_apply, Prod.map_fst, snd_prod, Prod.map_snd]
rw [← Function.comp_def, ← map_map, ← map_map, ← Function.comp_def f₂, ← map_map, ← map_map,
h₁.map_prod_eq_map_prod (by simpa using hsA.1) (by simpa using htA.1) (by simpa) (by simpa),
h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2) (by simpa [@forall_swap α₁] using htA.2)
(by simpa) (by simpa)]
