Commit 2026-02-18 12:06 ab58ce6f

View on Github →

feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps (#33397)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Star/LinearMap.lean

added theorem ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star

added theorem ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff

added theorem ContinuousLinearMap.intrinsicStar_apply

added theorem ContinuousLinearMap.intrinsicStar_comp'

added theorem ContinuousLinearMap.intrinsicStar_comp

added theorem ContinuousLinearMap.intrinsicStar_eq_comp

added theorem ContinuousLinearMap.intrinsicStar_id

added theorem ContinuousLinearMap.intrinsicStar_smulRight

added theorem ContinuousLinearMap.intrinsicStar_toSpanSingleton

added theorem ContinuousLinearMap.intrinsicStar_zero

added theorem ContinuousLinearMap.toLinearMap_intrinsicStar