Finset.map_prodComm_antidiagonal
theorem Finset.map_prodComm_antidiagonal :
∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A},
Finset.map (Equiv.prodComm A A).toEmbedding (Finset.antidiagonal n) = Finset.antidiagonal n
The theorem `Finset.map_prodComm_antidiagonal` states that for any type `A` that has an additive commutative monoid structure and a defined antidiagonal, and for any element `n` of type `A`, the image of the antidiagonal of `n` under the map defined by the embedding of the product commutativity equivalence (i.e., the transformation that swaps the components of pairs) is equal to the original antidiagonal of `n`. Essentially, this means that swapping the components of each pair in the antidiagonal of `n` results in the same set, highlighting the symmetry property of the antidiagonal in an additive commutative monoid.
More concisely: For any additive commutative monoid `A` with defined antidiagonal, the image of its antidiagonal under the product commutativity map is equal to the original antidiagonal.
|
Finset.antidiagonal_zero
theorem Finset.antidiagonal_zero :
∀ {A : Type u_1} [inst : CanonicallyOrderedAddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A],
Finset.antidiagonal 0 = {(0, 0)}
This theorem states that for any type `A` that is a canonically ordered additive commutative monoid and has an antidiagonal, the antidiagonal of `0` is the set containing only the pair `(0, 0)`. In more mathematical terms, if we consider an element from a set `A` that satisfies the properties of an additive commutative monoid with a canonical order and has the additional property of an antidiagonal, the antidiagonal of the additive identity (which is `0` in this context) is the set containing only the pair `(0, 0)`.
More concisely: For any additive commutative monoid `A` with a canonical order and an antidiagonal, the antidiagonal of `0` is the singleton set `{(0, 0)}`.
|
Mathlib.Data.Finset.Antidiagonal._auxLemma.1
theorem Mathlib.Data.Finset.Antidiagonal._auxLemma.1 :
∀ {A : Type u_1} [inst : AddMonoid A] [self : Finset.HasAntidiagonal A] {n : A} {a : A × A},
(a ∈ Finset.antidiagonal n) = (a.1 + a.2 = n)
This theorem, `Mathlib.Data.Finset.Antidiagonal._auxLemma.1`, states that for any type `A` which has an addition operation (from the `AddMonoid A` instance), and a defined `Finset.HasAntidiagonal` instance, a pair of elements (`a : A × A`) is in the antidiagonal of `n` if and only if the sum of the elements of the pair equals to `n`. The antidiagonal of `n` is a set of pairs whose sum is `n`.
More concisely: For any type `A` with an addition operation and a `Finset.HasAntidiagonal` instance, the antidiagonal of `n` is the set of pairs `(a, b)` in `A × A` such that `a + b = n`.
|
Finset.antidiagonal_congr'
theorem Finset.antidiagonal_congr' :
∀ {A : Type u_1} [inst : AddCancelCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {p q : A × A} {n : A},
p ∈ Finset.antidiagonal n → q ∈ Finset.antidiagonal n → (p = q ↔ p.2 = q.2)
This theorem states that for any given type `A`, which has an addition operation that is both cancellative and commutative and a defined antidiagonal, and for any two pairs of elements `p` and `q` from `A` and any element `n` from `A`. If both `p` and `q` belong to the antidiagonal of `n`, then `p` equals `q` if and only if the second element of `p` equals the second element of `q`. This theorem highlights the uniqueness of the second coordinate in determining a point on the antidiagonal of a set.
More concisely: For any commutative and cancellative additive type `A` with an antidiagonal, if two pairs `(p, p\_second)` and `(q, q\_second)` lie on the antidiagonal of an element `n`, then `p = q` if and only if `p_second = q_second`.
|
Finset.antidiagonal_subtype_ext
theorem Finset.antidiagonal_subtype_ext :
∀ {A : Type u_1} [inst : AddCancelMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A}
{p q : { x // x ∈ Finset.antidiagonal n }}, (↑p).1 = (↑q).1 → p = q
This theorem, `Finset.antidiagonal_subtype_ext`, states that, for any type `A` equipped with the structure of an `AddCancelMonoid` and a `Finset.HasAntidiagonal` relation, any natural number `n`, and any two points `p` and `q` in the antidiagonal set of `n`, if the first coordinates of `p` and `q` are equal, then `p` and `q` are equal. This theorem is used by the `ext` tactic and is a subtype version of the `Finset.antidiagonal_congr` theorem. The antidiagonal of a number `n` is the set of pairs `(a, b)` such that `a + b = n`.
More concisely: Given a type `A` with an `AddCancelMonoid` structure and a `Finset.HasAntidiagonal` relation, if `n` is a natural number and `p` and `q` are elements in the antidiagonal set of `n` with equal first coordinates, then `p` and `q` are equal.
|
Finset.map_swap_antidiagonal
theorem Finset.map_swap_antidiagonal :
∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A},
Finset.map { toFun := Prod.swap, inj' := ⋯ } (Finset.antidiagonal n) = Finset.antidiagonal n
This theorem states that for any type `A` that has an additive commutative monoid structure and a defined antidiagonal, and for any number `n` of type `A`, the image of the antidiagonal of `n` under the swapping function is equal to the antidiagonal of `n` itself. In other words, if you take pairs of elements `(a, b)` that add up to `n` (forming the antidiagonal), and if you swap the elements in each pair to get `(b, a)`, the set of pairs you end up with is still the antidiagonal of `n`. This is a result of the commutativity of the addition operation in `A`.
More concisely: For any additive commutative monoid `A` with defined antidiagonal, the swapped antidiagonal is equal to the original antidiagonal.
|
Finset.antidiagonal_congr
theorem Finset.antidiagonal_congr :
∀ {A : Type u_1} [inst : AddCancelMonoid A] [inst_1 : Finset.HasAntidiagonal A] {p q : A × A} {n : A},
p ∈ Finset.antidiagonal n → q ∈ Finset.antidiagonal n → (p = q ↔ p.1 = q.1)
This theorem states that for any type `A` that is an instance of the `AddCancelMonoid` and has an `antidiagonal` property, given any two pairs `p` and `q` of type `A`, and a value `n` of type `A`, if both `p` and `q` are in the antidiagonal of `n`, then `p` is equal to `q` if and only if the first element of `p` is equal to the first element of `q`. This theorem thereby states that a point in the antidiagonal is uniquely determined by its first coordinate.
More concisely: For any type `A` with `AddCancelMonoid` instance and `antidiagonal` property, if two pairs `(a, b)` and `(c, d)` in the antidiagonal of `n` have equal first coordinates, then `a = c` if and only if `b = d`.
|
Finset.HasAntidiagonal.mem_antidiagonal
theorem Finset.HasAntidiagonal.mem_antidiagonal :
∀ {A : Type u_1} [inst : AddMonoid A] [self : Finset.HasAntidiagonal A] {n : A} {a : A × A},
a ∈ Finset.antidiagonal n ↔ a.1 + a.2 = n
This theorem states that for any given type `A` that is an additive monoid, and given a pair of elements `a` of type `A`, that pair belongs to the antidiagonal set of `n` if and only if the sum of the components of the pair is equal to `n`. In simpler terms, a pair is in the antidiagonal of `n` precisely when the two elements of the pair add up to `n`.
More concisely: For any additive monoid type `A` and elements `a, b` of `A`, the pair `(a, b)` belongs to the antidiagonal set of `n` if and only if `a + b = n`.
|