Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-25 17:50
a71a4a3c
View on Github →
feat: port Analysis.NormedSpace.Star.Basic (
#3650
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/NormedSpace/Star/Basic.lean
added
theorem
CstarRing.mul_star_self_eq_zero_iff
added
theorem
CstarRing.mul_star_self_ne_zero_iff
added
theorem
CstarRing.nnnorm_self_mul_star
added
theorem
CstarRing.nnnorm_star_mul_self
added
theorem
CstarRing.norm_coe_unitary
added
theorem
CstarRing.norm_coe_unitary_mul
added
theorem
CstarRing.norm_mem_unitary_mul
added
theorem
CstarRing.norm_mul_coe_unitary
added
theorem
CstarRing.norm_mul_mem_unitary
added
theorem
CstarRing.norm_of_mem_unitary
added
theorem
CstarRing.norm_one
added
theorem
CstarRing.norm_self_mul_star
added
theorem
CstarRing.norm_star_mul_self'
added
theorem
CstarRing.norm_unitary_smul
added
theorem
CstarRing.star_mul_self_eq_zero_iff
added
theorem
CstarRing.star_mul_self_ne_zero_iff
added
theorem
IsSelfAdjoint.nnnorm_pow_two_pow
added
theorem
coe_starₗᵢ
added
theorem
nnnorm_star
added
theorem
selfAdjoint.nnnorm_pow_two_pow
added
def
starNormedAddGroupHom
added
theorem
star_isometry
added
def
starₗᵢ
added
theorem
starₗᵢ_apply