1 parent 0bd5dd7 commit accdf48Copy full SHA for accdf48
1 file changed
Mathlib/Data/List/TFAE.lean
@@ -13,8 +13,6 @@ public import Mathlib.Data.List.Pairwise
13
14
This file allows to state that all propositions in a list are equivalent. It is used by
15
`Mathlib/Tactic/Tfae.lean`.
16
-`TFAE l` means `∀ x ∈ l, ∀ y ∈ l, x ↔ y`. This is equivalent to `l.Pairwise (· ↔ ·)`, see
17
-`List.tfae_iff_pairwise`.
18
-/
19
20
@[expose] public section
0 commit comments