Commit 2025-06-04 13:46 6455ba8a

View on Github →

feat: define IsPositive and Löwner order for LinearMap (#24471) Moves:

ContinuousLinearMap.IsPositive.inner_nonneg_left -> ContinuousLinearMap.IsPositive.re_inner_nonneg_left
ContinuousLinearMap.IsPositive.inner_nonneg_right -> ContinuousLinearMap.IsPositive.re_inner_nonneg_right

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added theorem ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff

added theorem LinearMap.isSelfAdjoint_toContinuousLinearMap_iff

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

added theorem ContinuousLinearMap.IsPositive.inner_left_eq_inner_right

added theorem ContinuousLinearMap.IsPositive.re_inner_nonneg_left

added theorem ContinuousLinearMap.IsPositive.re_inner_nonneg_right

added theorem ContinuousLinearMap.isPositive_iff

added theorem ContinuousLinearMap.isPositive_natCast

added theorem ContinuousLinearMap.isPositive_ofNat

added theorem ContinuousLinearMap.isPositive_toLinearMap_iff

added theorem LinearMap.IsPositive.add

added theorem LinearMap.IsPositive.adjoint_conj

added theorem LinearMap.IsPositive.conj_adjoint

added theorem LinearMap.IsPositive.inner_nonneg_left

added theorem LinearMap.IsPositive.inner_nonneg_right

added theorem LinearMap.IsPositive.isSelfAdjoint

added theorem LinearMap.IsPositive.isSymmetric

added theorem LinearMap.IsPositive.re_inner_nonneg_left

added theorem LinearMap.IsPositive.re_inner_nonneg_right

added def LinearMap.IsPositive

added theorem LinearMap.isPositive_iff

added theorem LinearMap.isPositive_iff_complex

added theorem LinearMap.isPositive_natCast

added theorem LinearMap.isPositive_ofNat

added theorem LinearMap.isPositive_one

added theorem LinearMap.isPositive_toContinuousLinearMap_iff

added theorem LinearMap.isPositive_zero

added theorem LinearMap.le_def

added theorem LinearMap.nonneg_iff_isPositive

Modified Mathlib/Analysis/InnerProductSpace/StarOrder.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

added theorem LinearMap.IsSymmetric.coe_re_inner_apply_self

added theorem LinearMap.IsSymmetric.coe_re_inner_self_apply

added theorem LinearMap.IsSymmetric.im_inner_apply_self

added theorem LinearMap.IsSymmetric.im_inner_self_apply

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

added theorem ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap

added theorem LinearMap.toContinuousLinearMap_eq_iff_eq_toLinearMap