Theorem Combinatorics.Subspace.exists_mono_in_high_dimension_fin

Modification history

2024-07-30 00:05
Mathlib/Combinatorics/HalesJewett.lean
chore(Combinatorics/HalesJewett): replace Fintype -> Finite (#15279) …
Modified Combinatorics.Subspace.exists_mono_in_high_dimension_finView on Github →
2024-07-23 15:36
Mathlib/Combinatorics/HalesJewett.lean
feat: Combinatorial subspaces and multidimensional Hales-Jewett (#8304) …
Added Combinatorics.Subspace.exists_mono_in_high_dimension_finView on Github →