Skip to content

Commit d4830ba

Browse files
committed
chore(Data/Finsupp/Defs): remove redundant instances (#39938)
These instances seem quite redundant to me.
1 parent 33c530f commit d4830ba

1 file changed

Lines changed: 0 additions & 15 deletions

File tree

Mathlib/Data/DFinsupp/Defs.lean

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1123,21 +1123,6 @@ def equivCongrLeft [∀ i, Zero (β i)] (h : ι ≃ κ) : (Π₀ i, β i) ≃ Π
11231123
rw [comapDomain'_apply, mapRange_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
11241124
h.apply_symm_apply]
11251125

1126-
section SigmaCurry
1127-
1128-
variable {α : ι → Type*} {δ : ∀ i, α i → Type v}
1129-
1130-
instance hasAdd₂ [∀ i j, AddZeroClass (δ i j)] : Add (Π₀ (i : ι) (j : α i), δ i j) :=
1131-
inferInstance
1132-
1133-
instance addZeroClass₂ [∀ i j, AddZeroClass (δ i j)] : AddZeroClass (Π₀ (i : ι) (j : α i), δ i j) :=
1134-
inferInstance
1135-
1136-
instance addMonoid₂ [∀ i j, AddMonoid (δ i j)] : AddMonoid (Π₀ (i : ι) (j : α i), δ i j) :=
1137-
inferInstance
1138-
1139-
end SigmaCurry
1140-
11411126
variable {α : Option ι → Type v}
11421127

11431128
/-- Adds a term to a dfinsupp, making a dfinsupp indexed by an `Option`.

0 commit comments

Comments
 (0)