Theorem CFC.log_zero

Modification history

2025-10-20 11:16
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
chore: backport grind annotation changes from nightly-testing (#30572)
Modified CFC.log_zeroView on Github →
2025-09-26 11:53
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
feat: Define strictly positive operators (i.e. positive definite) (#29087)
Modified CFC.log_zeroView on Github →
2024-07-17 03:09
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
feat(ContinuousFunctionalCalculus): Define the real log based on the CFC (#14448) …
Added CFC.log_zeroView on Github →