Skip to content

Commit 6549fa3

Browse files
chore: deprecate duplicate zeta_mul_kappa lemma (#30055)
This PR deprecates the duplicate lemma `zeta_mul_kappa` that was identical to `zeta_mul_zeta` but with a typo in the name. Closes #28440.
1 parent bb6ed24 commit 6549fa3

1 file changed

Lines changed: 1 addition & 6 deletions

File tree

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -352,12 +352,7 @@ lemma zeta_mul_zeta [NonAssocSemiring 𝕜] [Preorder α] [LocallyFiniteOrder α
352352
rw [mem_Icc] at hx
353353
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
354354

355-
lemma zeta_mul_kappa [NonAssocSemiring 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableLE α]
356-
(a b : α) : (zeta 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) a b = (Icc a b).card := by
357-
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
358-
refine sum_congr rfl fun x hx ↦ ?_
359-
rw [mem_Icc] at hx
360-
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
355+
@[deprecated (since := "2025-09-28")] alias zeta_mul_kappa := zeta_mul_zeta
361356

362357
section Mu
363358
variable (𝕜) [AddCommGroup 𝕜] [One 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableEq α]

0 commit comments

Comments
 (0)