Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/Combinatorics/Additive/FreimanHom.lean
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ import Mathlib.Data.ZMod.Defs
/-!
# Freiman homomorphisms

In this file, we define Freiman homomorphisms and isomorphism.
In this file, we define Freiman homomorphisms and isomorphisms.

An `n`-Freiman homomorphism from `A` to `B` is a function `f : α → β` such that `f '' A ⊆ B` and
`f x₁ * ... * f xₙ = f y₁ * ... * f yₙ` for all `x₁, ..., xₙ, y₁, ..., yₙ ∈ A` such that
Expand Down Expand Up @@ -57,7 +57,7 @@ an `AddMonoid`/`Monoid` instead of the `AddMonoid`/`Monoid` itself.

* `MonoidHomClass.isMulFreimanHom` could be relaxed to `MulHom.toFreimanHom` by proving
`(s.map f).prod = (t.map f).prod` directly by induction instead of going through `f s.prod`.
* Affine maps are Freiman homs.
* Affine maps are Freiman homomorphisms.
-/

assert_not_exists Field Ideal TwoSidedIdeal
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Combinatorics/Enumerative/DyckWord.lean
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ structure DyckWord where
toList : List DyckStep
/-- There are as many `U`s as `D`s -/
count_U_eq_count_D : toList.count U = toList.count D
/-- Each prefix has as least as many `U`s as `D`s -/
/-- Each prefix has at least as many `U`s as `D`s -/
count_D_le_count_U i : (toList.take i).count D ≤ (toList.take i).count U
deriving DecidableEq

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Combinatorics/Quiver/Cast.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import Mathlib.Combinatorics.Quiver.Path

# Rewriting arrows and paths along vertex equalities

This files defines `Hom.cast` and `Path.cast` (and associated lemmas) in order to allow
This file defines `Hom.cast` and `Path.cast` (and associated lemmas) in order to allow
rewriting arrows and paths along equalities of their endpoints.

-/
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,12 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Powerset
# The Ahlswede-Zhang identity

This file proves the Ahlswede-Zhang identity, which is a nontrivial relation between the size of the
"truncated unions" of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality
"truncated unions" of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality
`Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose`, by making explicit the correction
term.

For a set family `𝒜` over a ground set of size `n`, the Ahlswede-Zhang identity states that the sum
of `|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|)` over all set `A` is exactly `1`. This implies the LYM
of `|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|)` over all sets `A` is exactly `1`. This implies the LYM
inequality since for an antichain `𝒜` and every `A ∈ 𝒜` we have
`|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) = 1 / n.choose |A|`.

Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,20 @@ A graph is complete multipartite iff non-adjacency is transitive.

## Main declarations

* `SimpleGraph.IsCompleteMultipartite`: predicate for a graph to be complete-multi-partite.
* `SimpleGraph.IsCompleteMultipartite`: predicate for a graph to be complete multipartite.

* `SimpleGraph.IsCompleteMultipartite.setoid`: the `Setoid` given by non-adjacency.

* `SimpleGraph.IsCompleteMultipartite.iso`: the graph isomorphism from a graph that
`IsCompleteMultipartite` to the corresponding `completeMultipartiteGraph`.

* `SimpleGraph.IsPathGraph3Compl`: predicate for three vertices to be a witness to
non-complete-multi-partite-ness of a graph G. (The name refers to the fact that the three
* `SimpleGraph.IsPathGraph3Compl`: predicate for three vertices to witness the
non-complete-multipartiteness of a graph `G`. (The name refers to the fact that the three
vertices form the complement of `pathGraph 3`.)

* See also: `Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean`
`colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree` a maximally `r + 1`- cliquefree graph
is `r`-colorable iff it is complete-multipartite.
* See also: `Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean`.
The lemma `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree` states that a maximally
`r + 1`-cliquefree graph is `r`-colorable iff it is complete multipartite.

* `SimpleGraph.completeEquipartiteGraph`: the **complete equipartite graph** in parts of *equal*
size such that two vertices are adjacent if and only if they are in different parts.
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Mathlib.Data.Fin.Parity
/-!
# Concrete colorings of common graphs

This file defines colorings for some common graphs
This file defines colorings for some common graphs.

## Main declarations

Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Combinatorics/SimpleGraph/Copy.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,12 @@ import Mathlib.Combinatorics.SimpleGraph.Subgraph

This file introduces the concept of one simple graph containing a copy of another.

For two simple graph `G` and `H`, a *copy* of `G` in `H` is a (not necessarily induced) subgraph of
For two simple graphs `G` and `H`, a *copy* of `G` in `H` is a (not necessarily induced) subgraph of
`H` isomorphic to `G`.

If there exists a copy of `G` in `H`, we say that `H` *contains* `G`. This is equivalent to saying
that there is an injective graph homomorphism `G → H` them (this is **not** the same as a graph
embedding, as we do not require the subgraph to be induced).
that there is an injective graph homomorphism `G → H` between them (this is **not** the same as a
graph embedding, as we do not require the subgraph to be induced).

If there exists an induced copy of `G` in `H`, we say that `H` *inducingly contains* `G`. This is
equivalent to saying that there is a graph embedding `G ↪ H`.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Mathlib.Data.Nat.Choose.Cast
/-!
# Turán density
This files defines the **Turán density** of a simple graph.
This file defines the **Turán density** of a simple graph.
## Main definitions
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
Original file line number Diff line number Diff line change
Expand Up @@ -110,8 +110,8 @@ private lemma IsNClique.insert_insert_erase (hs : G.IsNClique r (insert a s)) (h
An `IsFiveWheelLike r k v w₁ w₂ s t` structure in `G` consists of vertices `v w₁ w₂` and `r`-sets
`s` and `t` such that `{v, w₁, w₂}` induces the single edge `w₁w₂` (i.e. they form an
`IsPathGraph3Compl`), `v, w₁, w₂ ∉ s ∪ t`, `s ∪ {v}, t ∪ {v}, s ∪ {w₁}, t ∪ {w₂}` are all
`(r + 1)`- cliques and `#(s ∩ t) = k`. (If `G` is maximally `(r + 2)`-cliquefree and not complete
multipartite then `G` will contain such a structure : see
`(r + 1)`-cliques and `#(s ∩ t) = k`. (If `G` is maximally `(r + 2)`-cliquefree and not complete
multipartite then `G` will contain such a structure: see
`exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`.)
-/
@[grind]
Expand Down Expand Up @@ -357,7 +357,7 @@ lemma minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ [Fintype α]
obtain ⟨_, _, hW⟩ := hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf
(by simpa [X] using hx) <| Nat.le_of_succ_le_succ h
exact hm hW
-- Since `G` is `Kᵣ₊₂`- free and contains a `Wᵣ,ₖ` every vertex is not adjacent to at least one
-- Since `G` is `Kᵣ₊₂`-free and contains a `Wᵣ,ₖ`, every vertex is not adjacent to at least one
-- wheel vertex.
have one_le (x : α) : 1 ≤ #{z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬ G.Adj x z} :=
let ⟨_, hz⟩ := hw.isNClique_fst_left.exists_not_adj_of_cliqueFree_succ hcf x
Expand Down