Commit 2026-05-20 02:56 66916540

View on Github →

feat(Analysis): more LinearIsometryEquiv API (#39144) From MeanFourier

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

added theorem enorm_map'

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

deleted theorem LinearIsometry.enorm_map

deleted theorem LinearIsometry.nnnorm_map

deleted theorem LinearIsometry.norm_map

deleted theorem LinearIsometryEquiv.nnnorm_map

deleted theorem LinearIsometryEquiv.norm_map

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_inv

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_mul

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_one

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearEquiv.toContinuousLinearMap_mul

added theorem ContinuousLinearEquiv.toContinuousLinearMap_one

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem ContinuousLinearMap.mk_id

added theorem ContinuousLinearMap.mk_one