Commit 2026-04-14 12:34 02ac6c3c

View on Github →

chore(Analysis): golf Basic, Exponential, and ContinuousFunctionalCalculus/Unique (#38006) Split from #37987 at reviewer request. This PR contains only the golf changes to:

Mathlib/Analysis/CStarAlgebra/Basic.lean
Mathlib/Analysis/CStarAlgebra/Exponential.lean
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean Requested in: https://github.com/leanprover-community/mathlib4/pull/37987#discussion_r3073812894

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/Basic.lean

modified theorem CStarRing.norm_mul_coe_unitary

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

Modified Mathlib/Analysis/CStarAlgebra/Exponential.lean