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