Commit 2023-05-26 23:07 91459584

View on Github →

feat: port Analysis.InnerProductSpace.Dual (#4402)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Dual.lean

added def InnerProductSpace.continuousLinearMapOfBilin

added theorem InnerProductSpace.continuousLinearMapOfBilin_apply

added theorem InnerProductSpace.ext_inner_left_basis

added theorem InnerProductSpace.ext_inner_right_basis

added theorem InnerProductSpace.innerSL_norm

added def InnerProductSpace.toDual

added def InnerProductSpace.toDualMap

added theorem InnerProductSpace.toDualMap_apply

added theorem InnerProductSpace.toDual_apply

added theorem InnerProductSpace.toDual_symm_apply

added theorem InnerProductSpace.unique_continuousLinearMapOfBilin