Skip to content

Commit 3d9f34a

Browse files
committed
chore(Data/Finsupp): add deprecations for leanprover-community#32074 (leanprover-community#32650)
The lemmas `Finsupp.degree_add` and `Finsupp.degree_zero` were removed in leanprover-community#32074 without deprecation.
1 parent 5bdc13f commit 3d9f34a

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

Mathlib/Data/Finsupp/Weight.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -210,6 +210,10 @@ def degree : (σ →₀ R) →+ R where
210210
map_zero' := by simp
211211
map_add' := fun _ _ => sum_add_index' (h := fun _ ↦ id) (congrFun rfl) fun _ _ ↦ congrFun rfl
212212

213+
@[deprecated (since := "2025-12-09")] alias degree_add := map_add
214+
215+
@[deprecated (since := "2025-12-09")] alias degree_zero := map_zero
216+
213217
theorem degree_apply (d : σ →₀ R) : degree d = ∑ i ∈ d.support, d i := rfl
214218

215219
theorem degree_eq_sum [Fintype σ] (f : σ →₀ R) : f.degree = ∑ i, f i := by

0 commit comments

Comments
 (0)