Commit 2024-08-31 15:30 a2abea1e

View on Github →

feat: in a unital C⋆-algebra, ‖a‖ ≤ r ↔ a ≤ r • 1, and related lemmas (#16266)

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

added theorem CFC.exists_pos_algebraMap_le_iff

modified theorem CStarRing.conjugate_le_norm_smul'

modified theorem CStarRing.conjugate_le_norm_smul

added theorem CStarRing.nnnorm_le_iff_of_nonneg

added theorem CStarRing.nnnorm_le_natCast_iff_of_nonneg

added theorem CStarRing.nnnorm_le_one_iff_of_nonneg

modified theorem CStarRing.nnnorm_mem_spectrum_of_nonneg

added theorem CStarRing.norm_le_iff_le_algebraMap

added theorem CStarRing.norm_le_natCast_iff_of_nonneg

modified theorem CStarRing.norm_le_norm_of_nonneg_of_le

added theorem CStarRing.norm_le_one_iff_of_nonneg

modified theorem CStarRing.norm_mem_spectrum_of_nonneg

modified theorem CStarRing.norm_or_neg_norm_mem_spectrum

added theorem cfc_nnreal_le_iff

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

added theorem CFC.le_one

added theorem CFC.le_one_iff

added theorem CFC.one_le

added theorem CFC.one_le_iff

added theorem algebraMap_le_cfc_iff

added theorem algebraMap_le_iff_le_spectrum

added theorem cfc_le_algebraMap_iff

added theorem cfc_le_one_iff

added theorem le_algebraMap_iff_spectrum_le

added theorem one_le_cfc_iff

Modified Mathlib/Topology/Instances/NNReal.lean

added theorem ContinuousOn.ofReal_map_toNNReal