Commit 2023-06-01 13:13 34e8b42c

View on Github →

feat: port Analysis.InnerProductSpace.Adjoint (#4476)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added def ContinuousLinearMap.adjoint

added def ContinuousLinearMap.adjointAux

added theorem ContinuousLinearMap.adjointAux_adjointAux

added theorem ContinuousLinearMap.adjointAux_apply

added theorem ContinuousLinearMap.adjointAux_inner_left

added theorem ContinuousLinearMap.adjointAux_inner_right

added theorem ContinuousLinearMap.adjointAux_norm

added theorem ContinuousLinearMap.adjoint_adjoint

added theorem ContinuousLinearMap.adjoint_comp

added theorem ContinuousLinearMap.adjoint_id

added theorem ContinuousLinearMap.adjoint_inner_left

added theorem ContinuousLinearMap.adjoint_inner_right

added theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left

added theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right

added theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left

added theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right

added theorem ContinuousLinearMap.eq_adjoint_iff

added theorem ContinuousLinearMap.isAdjointPair_inner

added theorem ContinuousLinearMap.isSelfAdjoint_iff'

added theorem ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric

added theorem ContinuousLinearMap.star_eq_adjoint

added theorem IsSelfAdjoint.adjoint_conj

added theorem IsSelfAdjoint.adjoint_eq

added theorem IsSelfAdjoint.conj_adjoint

added theorem IsSelfAdjoint.conj_orthogonalProjection

added theorem IsSelfAdjoint.isSymmetric

added theorem LinearMap.IsSymmetric.coe_toSelfAdjoint

added theorem LinearMap.IsSymmetric.isSelfAdjoint

added def LinearMap.IsSymmetric.toSelfAdjoint

added theorem LinearMap.IsSymmetric.toSelfAdjoint_apply

added def LinearMap.adjoint

added theorem LinearMap.adjoint_adjoint

added theorem LinearMap.adjoint_comp

added theorem LinearMap.adjoint_eq_toClm_adjoint

added theorem LinearMap.adjoint_inner_left

added theorem LinearMap.adjoint_inner_right

added theorem LinearMap.adjoint_toContinuousLinearMap

added theorem LinearMap.eq_adjoint_iff

added theorem LinearMap.eq_adjoint_iff_basis

added theorem LinearMap.eq_adjoint_iff_basis_left

added theorem LinearMap.eq_adjoint_iff_basis_right

added theorem LinearMap.im_inner_adjoint_mul_self_eq_zero

added theorem LinearMap.isAdjointPair_inner

added theorem LinearMap.isSelfAdjoint_iff'

added theorem LinearMap.isSymmetric_adjoint_mul_self

added theorem LinearMap.isSymmetric_iff_isSelfAdjoint

added theorem LinearMap.re_inner_adjoint_mul_self_nonneg

added theorem LinearMap.star_eq_adjoint

added theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint

added theorem Submodule.adjoint_orthogonalProjection

added theorem Submodule.adjoint_subtypeL

added theorem orthogonalProjection_isSelfAdjoint