From 8c811c94af285516e8c76a63165c87027f18ccd0 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Mon, 9 Sep 2024 02:15:52 +0000 Subject: [PATCH] =?UTF-8?q?fix:=20`Finpartition.atomise`=20should=20not=20?= =?UTF-8?q?have=20`[Fintype=20=CE=B1]`=20(#16617)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Noticed by @b-mehta. --- Mathlib/Order/Partition/Finpartition.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Order/Partition/Finpartition.lean b/Mathlib/Order/Partition/Finpartition.lean index de3531685cda0..abdda3c97c4c7 100644 --- a/Mathlib/Order/Partition/Finpartition.lean +++ b/Mathlib/Order/Partition/Finpartition.lean @@ -548,6 +548,8 @@ lemma card_mod_card_parts_le : s.card % P.parts.card ≤ P.parts.card := by rw [h, h'] · exact (Nat.mod_lt _ h).le +section Setoid + variable [Fintype α] /-- A setoid over a finite type induces a finpartition of the type's elements, @@ -587,6 +589,8 @@ theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} : simp only [← hc, mem_univ, mem_filter, true_and] at this ⊢ exact ⟨s.trans (s.symm this), s.trans this⟩ +end Setoid + section Atomise /-- Cuts `s` along the finsets in `F`: Two elements of `s` will be in the same part if they are