Mathlib Changelog
v4
Changelog
About
Github
Theorem
norm_cfcₙ_one_sub_one_add_inv_lt_one
Modification history
2024-10-30 16:54
Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
feat: positive contractions in a C⋆-algebra form a directed set (#18016)
Added
norm_cfcₙ_one_sub_one_add_inv_lt_one
View on Github →