From 332b6cd7794f09d3b74b310d159f1735ac6e7ffa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 28 Sep 2024 17:13:45 +0000 Subject: [PATCH] chore(Finset/Density): Fix statement and make lemmas simp (#17227) From LeanAPAP --- Mathlib/Data/Finset/Density.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean index 43125f7fcc4f3..002513c40e808 100644 --- a/Mathlib/Data/Finset/Density.lean +++ b/Mathlib/Data/Finset/Density.lean @@ -110,23 +110,23 @@ lemma dens_image [Fintype β] [DecidableEq β] {f : α → β} (hf : Bijective f (s.image f).dens = s.dens := by simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf) -lemma card_mul_dens (s : Finset α) : Fintype.card α * s.dens = s.card := by +@[simp] lemma card_mul_dens (s : Finset α) : Fintype.card α * s.dens = s.card := by cases isEmpty_or_nonempty α · simp [Subsingleton.elim s ∅] rw [dens, mul_div_cancel₀] exact mod_cast Fintype.card_ne_zero -lemma dens_mul_card (s : Finset α) : s.dens * Fintype.card α = s.card := by +@[simp] lemma dens_mul_card (s : Finset α) : s.dens * Fintype.card α = s.card := by rw [mul_comm, card_mul_dens] section Semifield variable [Semifield 𝕜] [CharZero 𝕜] -lemma natCast_card_mul_nnratCast_dens (s : Finset α) : (Fintype.card α * s.dens : 𝕜) = s.card := - mod_cast s.card_mul_dens +@[simp] lemma natCast_card_mul_nnratCast_dens (s : Finset α) : + (Fintype.card α * s.dens : 𝕜) = s.card := mod_cast s.card_mul_dens -lemma nnratCast_dens_mul_natCast_card (s : Finset α) : s.dens * Fintype.card α = s.card := - mod_cast s.dens_mul_card +@[simp] lemma nnratCast_dens_mul_natCast_card (s : Finset α) : + (s.dens * Fintype.card α : 𝕜) = s.card := mod_cast s.dens_mul_card @[norm_cast] lemma nnratCast_dens (s : Finset α) : (s.dens : 𝕜) = s.card / Fintype.card α := by simp [dens]