Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-09 00:58
8a8bd683
View on Github →
chore: backports for leanprover/lean4
#4814
(part 38) (
#15618
)
Estimated changes
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
modified
theorem
StarOrderedRing.nonneg_iff_quasispectrum_nonneg
modified
theorem
cfcₙHom_nonneg_iff
modified
theorem
cfcₙ_nonneg_iff
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
modified
theorem
StarOrderedRing.nonneg_iff_spectrum_nonneg
modified
theorem
Units.continuousOn_zpow₀_spectrum
modified
theorem
cfcHom_nonneg_iff
modified
theorem
cfc_const_one
modified
theorem
cfc_eq_cfc_iff_eqOn
modified
theorem
cfc_nonneg_iff
modified
theorem
cfc_one
modified
theorem
cfc_star_id
modified
theorem
isUnit_cfc_iff