From 36eb824f665d1359a4c5b4d1d71cccb2d7161a04 Mon Sep 17 00:00:00 2001 From: blizzard_inc Date: Wed, 22 Jan 2025 21:31:30 +0100 Subject: [PATCH] Update Mathlib/Algebra/FreeMonoid/Count.lean Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> --- Mathlib/Algebra/FreeMonoid/Count.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/FreeMonoid/Count.lean b/Mathlib/Algebra/FreeMonoid/Count.lean index 7f2825d900230..b6bf22dd9c21f 100644 --- a/Mathlib/Algebra/FreeMonoid/Count.lean +++ b/Mathlib/Algebra/FreeMonoid/Count.lean @@ -44,7 +44,7 @@ theorem countP_apply (l : FreeMonoid α) : l.countP p = .ofAdd (l.toList.countP lemma countP_of (x : α) : (of x).countP p = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)] - simp only [decide_eq_true_eq, ofAdd_zero] + simp only [decide_eq_true_eq] /-- `List.count` as a bundled additive monoid homomorphism. -/