Commit 2026-03-06 08:34 5a04c9cf

View on Github →

feat: (continuous) bilinear map (#36193) On the path towards Riemannian geometry.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added def IsBilinearMap.toLinearMap

added structure IsBilinearMap

Created Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean

added def ContinuousLinearMap.evalL

added theorem ContinuousLinearMap.evalL_apply

added def IsBilinearMap.toContinuousBilinearMap

added theorem IsBilinearMap.toContinuousBilinearMap_apply

added def LinearMap.toContinuousBilinearMap

added theorem LinearMap.toContinuousBilinearMap_apply