Commit 2024-01-09 02:35 ef72bdbf

View on Github →

feat(Analysis/InnerProductSpace/Adjoint): add norm_adjoint_comp_self (#9569) This is a non-square version of norm_star_mul_self

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

modified theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left

modified theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right

modified theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left

modified theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right

added theorem ContinuousLinearMap.norm_adjoint_comp_self