English
Product congruence: given isomorphisms f: M ≃* M' and g: N ≃* N', there is a product isomorphism f × g : M × N ≃* M' × N'.
Русский
Конгруэнтность произведения: при задании изоморфизмов f: M ≃* M' и g: N ≃* N' существует произведение-изоморфизм f × g : M × N ≃* M' × N'.
LaTeX
$$$\\text{prodCongr} : (M \\simeq_* M') \\times (N \\simeq_* N') \\to (M \\times N) \\simeq_* (M' \\times N')$$$
Lean4
/-- Product of multiplicative isomorphisms; the maps come from `Equiv.prodCongr`. -/
@[to_additive prodCongr /-- Product of additive isomorphisms; the maps come from `Equiv.prodCongr`. -/
]
def prodCongr (f : M ≃* M') (g : N ≃* N') : M × N ≃* M' × N' :=
{ f.toEquiv.prodCongr g.toEquiv with map_mul' := fun _ _ => Prod.ext (map_mul f _ _) (map_mul g _ _) }
