Commit 2023-06-11 14:53 50d067d2

View on Github →

feat: port Analysis.NormedSpace.Algebra (#4971)

depends on: #4946

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Algebra.lean

added theorem WeakDual.CharacterSpace.norm_le_norm_one