English
For a finite list l in α, the NNReal norm of the product equals the product of the NNReal norms: ‖l.prod‖₊ = ∏ b ∈ l ‖b‖₊.
Русский
Для конечного списка l из элементов α NNReal-норма произведения равна произведению NNReal-норм элементов списка.
LaTeX
$$$\\|\\mathrm{prod}\\,l\\|_{+} = \\prod_{b\\in l} \\|b\\|_{+}$$$
Lean4
/-- A non-unital ring homomorphism from a `CommRing` to a `SeminormedRing` induces a
`SeminormedCommRing` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [CommRing R] [SeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) : SeminormedCommRing R :=
{ NonUnitalSeminormedRing.induced R S f, SeminormedAddCommGroup.induced R S f, ‹CommRing R› with }
