File tree Expand file tree Collapse file tree
FormalConjecturesForMathlib
FormalConjecturesTest/ForMathlib/Combinatorics/Additive Expand file tree Collapse file tree Original file line number Diff line number Diff line change 1+ /-
2+ Copyright 2026 The Formal Conjectures Authors.
3+
4+ Licensed under the Apache License, Version 2.0 (the "License");
5+ you may not use this file except in compliance with the License.
6+ You may obtain a copy of the License at
7+
8+ https://www.apache.org/licenses/LICENSE-2.0
9+
10+ Unless required by applicable law or agreed to in writing, software
11+ distributed under the License is distributed on an "AS IS" BASIS,
12+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+ See the License for the specific language governing permissions and
14+ limitations under the License.
15+ -/
16+
117import Mathlib
218
319noncomputable def maxCosetDim (K V : Type *) [DivisionRing K] [AddCommGroup V] [Module K V]
Original file line number Diff line number Diff line change 1+ /-
2+ Copyright 2026 The Formal Conjectures Authors.
3+
4+ Licensed under the Apache License, Version 2.0 (the "License");
5+ you may not use this file except in compliance with the License.
6+ You may obtain a copy of the License at
7+
8+ https://www.apache.org/licenses/LICENSE-2.0
9+
10+ Unless required by applicable law or agreed to in writing, software
11+ distributed under the License is distributed on an "AS IS" BASIS,
12+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+ See the License for the specific language governing permissions and
14+ limitations under the License.
15+ -/
16+
117import Mathlib
218
319/-- The boolean hypercube $G = \mathbb{F}_2^n = (\mathbb{Z}/2\mathbb{Z})^n$. -/
Original file line number Diff line number Diff line change 1+ /-
2+ Copyright 2026 The Formal Conjectures Authors.
3+
4+ Licensed under the Apache License, Version 2.0 (the "License");
5+ you may not use this file except in compliance with the License.
6+ You may obtain a copy of the License at
7+
8+ https://www.apache.org/licenses/LICENSE-2.0
9+
10+ Unless required by applicable law or agreed to in writing, software
11+ distributed under the License is distributed on an "AS IS" BASIS,
12+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+ See the License for the specific language governing permissions and
14+ limitations under the License.
15+ -/
16+
117import Mathlib
218import FormalConjecturesForMathlib.Combinatorics.Additive.Coset
319
You can’t perform that action at this time.
0 commit comments