Commit 2025-02-13 16:50 05ff91b6

View on Github →

feat(Pairwise): add Pairwise.rel_head_tail etc (#21773)

Estimated changes

Modified Mathlib/Data/List/Pairwise.lean

added theorem List.Pairwise.rel_head

added theorem List.Pairwise.rel_head_of_rel_head_head

added theorem List.Pairwise.rel_head_tail

modified theorem List.pairwise_of_reflexive_of_forall_ne