English
If E and F are normed commutative groups, their product E × F inherits a norm making it a normed commutative group, with the product operations commuting as usual.
Русский
Если E и F — нормированные коммутативные группы, их произведение E × F получает норму, делая его нормированной коммутативной группой, при этом операции умножения коммутируют как обычно.
LaTeX
$$$\text{Prod}(E,F)\text{ is a }\text{NormedCommGroup with } \| (x,y) \| = \max(\|x\|,\|y\|)$$$
Lean4
/-- Product of normed groups, using the sup norm. -/
@[to_additive /-- Product of normed groups, using the sup norm. -/
]
instance normedCommGroup [NormedCommGroup E] [NormedCommGroup F] : NormedCommGroup (E × F) :=
{ Prod.seminormedGroup with
mul_comm := mul_comm
eq_of_dist_eq_zero := eq_of_dist_eq_zero }
