Theorem Combinatorics.Line.apply_of_ne_none

Modification history

2024-07-23 15:36
Mathlib/Combinatorics/HalesJewett.lean
feat: Combinatorial subspaces and multidimensional Hales-Jewett (#8304) …
Deleted Combinatorics.Line.apply_of_ne_noneView on Github →
2023-02-21 09:26
Mathlib/Combinatorics/HalesJewett.lean
feat: port Combinatorics.HalesJewett (#1704)
Added Combinatorics.Line.apply_of_ne_noneView on Github →