Skip to content

Commit

Permalink
chore(DFinsupp/Basic): drop a DecidableEq assumption (#11795)
Browse files Browse the repository at this point in the history
Golf `DFinsupp.finite_support`,
drop an unneeded `DecidableEq` assumption.
  • Loading branch information
urkud authored and atarnoam committed Apr 16, 2024
1 parent 2f62498 commit 7ef4643
Showing 1 changed file with 4 additions and 6 deletions.
10 changes: 4 additions & 6 deletions Mathlib/Data/DFinsupp/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -560,17 +560,15 @@ theorem subtypeDomain_sub [∀ i, AddGroup (β i)] {p : ι → Prop} [DecidableP

end FilterAndSubtypeDomain

variable [dec : DecidableEq ι]
variable [DecidableEq ι]

section Basic

variable [∀ i, Zero (β i)]

theorem finite_support (f : Π₀ i, β i) : Set.Finite { i | f i ≠ 0 } := by
classical
exact Trunc.induction_on f.support' fun xs =>
(Multiset.toFinset xs.1).finite_toSet.subset fun i H =>
Multiset.mem_toFinset.2 ((xs.prop i).resolve_right H)
theorem finite_support (f : Π₀ i, β i) : Set.Finite { i | f i ≠ 0 } :=
Trunc.induction_on f.support' fun xs ↦
xs.1.finite_toSet.subset fun i H ↦ ((xs.prop i).resolve_right H)
#align dfinsupp.finite_support DFinsupp.finite_support

/-- Create an element of `Π₀ i, β i` from a finset `s` and a function `x`
Expand Down

0 comments on commit 7ef4643

Please sign in to comment.