Commit 2025-03-16 14:08 bce45b1a

View on Github →

chore: move List.Lex lemmas out of the List.Lex namespace (#22935) This better matches the naming convention.

Estimated changes

Modified Mathlib/Data/List/Lex.lean

deleted theorem List.Lex.cons_iff

deleted theorem List.Lex.nil_left_or_eq_nil

deleted theorem List.Lex.singleton_iff

added theorem List.lex_cons_iff

added theorem List.lex_nil_or_eq_nil

added theorem List.lex_singleton_iff

Modified Mathlib/Data/String/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean