List.Palindrome.of_reverse_eq
theorem List.Palindrome.of_reverse_eq : ∀ {α : Type u_1} {l : List α}, l.reverse = l → l.Palindrome
This theorem states that for any type `α` and any list `l` of type `α`, if the reverse of `l` is equal to `l` itself, then `l` is a Palindrome. In other words, a list is a Palindrome if and only if it remains the same when its elements are reversed.
More concisely: For any list `l` of type `α`, `l` is a palindrome if and only if `l` is equal to its reverse.
|
List.Palindrome.reverse_eq
theorem List.Palindrome.reverse_eq : ∀ {α : Type u_1} {l : List α}, l.Palindrome → l.reverse = l
This theorem states that for any type `α` and a list `l` of type `α`, if the list `l` is a palindrome, then the reverse of the list `l` is equal to the list `l` itself. In other words, for a palindromic list, reversing the list doesn't change the list.
More concisely: If `α` is a type and `l` is a list of `α` that is a palindrome, then `l = reverse l`.
|