Theorem nnnorm_mul

Modification history

2025-03-25 09:42

Mathlib/Analysis/Normed/Field/Basic.lean

feat(Analysis/Normed): Class for strict multiplicativity of norm (#22842) …

Modified nnnorm_mul View on Github →

2025-01-23 07:42

Mathlib/Analysis/Normed/Field/Basic.lean

feat: more lemmas for `enorm` (#20966) …

Modified nnnorm_mul View on Github →

2023-03-13 13:27

Mathlib/Analysis/Normed/Field/Basic.lean

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

Added nnnorm_mul View on Github →