Commit 2025-08-12 12:14 522f23d6

View on Github →

chore(Data/List/Chain): rename chain'_cons to chain'_cons_cons (#28281) As suggested in this discussion, this PR renames chain'_cons to chain'_cons_cons and analogously Chain'.cons to Chain'.cons_cons.

Estimated changes

Modified Archive/Imo/Imo2024Q5.lean

Modified Mathlib/Data/List/Chain.lean

deleted theorem List.Chain'.cons

added theorem List.Chain'.cons_cons

deleted theorem List.chain'_cons

added theorem List.chain'_cons_cons

Modified Mathlib/GroupTheory/CoprodI.lean

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