Theorem norm_prod

Modification history

2024-05-27 08:32

Mathlib/Analysis/Normed/Field/Basic.lean

chore: Use the new `∑ i ∈ s, f i` notation (#13209) …

Modified norm_prod View on Github →

2023-03-13 13:27

Mathlib/Analysis/Normed/Field/Basic.lean

feat: port Analysis.Normed.Field.Basic (#2792)

Added norm_prod View on Github →