Commit 2025-06-05 07:31 d2867d7b

View on Github →

feat: construct an inner product space structure on a space already with a topology (#25398)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Defs.lean

added def InnerProductSpace.Core.toNormedAddCommGroupOfTopology

added theorem InnerProductSpace.Core.toNormedSpaceCore

added def InnerProductSpace.Core.toNormedSpaceOfTopology

deleted def InnerProductSpace.Core.toSeminormedSpace

added theorem InnerProductSpace.Core.toSeminormedSpaceCore

added theorem InnerProductSpace.Core.topology_eq

added def InnerProductSpace.ofCoreOfTopology

Modified Mathlib/Analysis/Normed/Module/Basic.lean

deleted structure SeminormedAddCommGroup.Core

added structure SeminormedSpace.Core