Skip to content

Commit fe51f22

Browse files
committed
chore: add deprecation (leanprover-community#31636)
This PR adds a deprecation to the file `Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog`, which was moved to its own folder in leanprover-community#31626.
1 parent 55116f9 commit fe51f22

File tree

2 files changed

+9
-0
lines changed

2 files changed

+9
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2022,6 +2022,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log
20222022
import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
20232023
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
20242024
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
2025+
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog
20252026
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
20262027
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
20272028
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
/-
2+
Copyright (c) 2024 Frédéric Dupuis. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Frédéric Dupuis
5+
-/
6+
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
7+
8+
deprecated_module (since := "2025-11-15")

0 commit comments

Comments
 (0)