Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 02ba894

Browse files
committed
chore (data/finset/sym): remove unnecessary alias (#18603)
See the discussion in this [PR](leanprover-community/mathlib4#2168)
1 parent 9f0d61b commit 02ba894

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

src/data/finset/sym.lean

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -141,10 +141,6 @@ end
141141
@[simp] lemma sym_nonempty : (s.sym n).nonempty ↔ n = 0 ∨ s.nonempty :=
142142
by simp_rw [nonempty_iff_ne_empty, ne.def, sym_eq_empty, not_and_distrib, not_ne_iff]
143143

144-
alias sym_nonempty ↔ _ nonempty.sym
145-
146-
attribute [protected] nonempty.sym
147-
148144
@[simp] lemma sym_univ [fintype α] (n : ℕ) : (univ : finset α).sym n = univ :=
149145
eq_univ_iff_forall.2 $ λ s, mem_sym_iff.2 $ λ a _, mem_univ _
150146

0 commit comments

Comments
 (0)