…15357)

Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

…15357)

Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

commit 9ef973d
Merge: 0bf4baf c3a48ab
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 20:41:16 2024 +0200

    Merge remote-tracking branch 'origin/master' into test/merge_assert_up

commit c3a48ab
Author: Jakob von Raumer <jakob@von-raumer.de>
Date:   Mon Aug 12 17:47:56 2024 +0000

    feat(CategoryTheory): Composing `Comma.map` with `Comma.fst` and `Comma.snd` (#15730)

commit 795a856
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 16:50:11 2024 +0000

    chore: uncomment some now viable assert_not_exists (#15715)

    Per [zulip](https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/.60assert_not_exists.60.20at.20top.20or.20bottom.20of.20file.3F/near/459960523) discussion.

    Co-authored-by: adomani <adomani@gmail.com>
    Co-authored-by: Johan Commelin <johan@commelin.net>

commit 0bf4baf
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 18:36:54 2024 +0200

    reorders

commit f2cd6ef
Author: Etienne <etienne.marion@ens-lyon.fr>
Date:   Mon Aug 12 16:36:26 2024 +0000

    doc: Add a note on how to use `CompactlyGeneratedSpace` (#15132)

    Following this discussion : https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Compactly.20generated.20spaces/near/453958229.
    Indicate that `CompactlyGeneratedSpace` should be used with an explicit universe parameter.

commit 09c4c46
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 18:33:33 2024 +0200

    dedups

commit d75c706
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 17:46:41 2024 +0200

    small fixes

commit d6d9c22
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Mon Aug 12 15:39:15 2024 +0000

    chore: remove unnecessary _root_ qualifications (#15704)

commit 821f584
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 17:31:21 2024 +0200

    fix one

commit 75da87b
Author: grunweg <rothgami@math.hu-berlin.de>
Date:   Mon Aug 12 15:28:15 2024 +0000

    perf(Geometry/Manifold/Instances/Sphere): speed up (#15488)

    Speed up the file by 9% by doing the following
    - squeeze simps where the full form is short and this is a clear win
    - "squeeze" three really slow field_simp calls: replace them by the equivalent simp invocation and squeeze that
    - avoid one slow `convert`
    - squeeze two really slow nlinarith calls (they're still slow, but much better)
    - replace one congr! by congr

    This is a reduced version of #13456, which is hopefully less controversial.

commit eb19004
Author: grunweg <rothgami@math.hu-berlin.de>
Date:   Mon Aug 12 15:28:14 2024 +0000

    perf(Geometry/Euclidean): squeeze slow field_simp calls (#13497)

    Replace them by the equivalent `simp` call and squeeze that. We leave `field_simp` calls slower than roughly 150ms in place. A few calls cannot easily be replaced; we leave these alone as well.

    Speeds up all affected files, including `Euclidean/Circumcenter` by 4%, `Inversion/Basic` by 27% and `Triangle` by 52%.

commit 2215b9e
Author: Ralf Stephan <ralf@ark.in-berlin.de>
Date:   Mon Aug 12 15:04:35 2024 +0000

    doc(Tactics): fix typo (#15739)

    Fix minor typo in `compute_degree` docstring.

commit f57201f
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date:   Mon Aug 12 15:04:34 2024 +0000

    chore: deduplicate `inv_mul_cancel`/`mul_inv_cancel`, etc. (#15717)

    * `mul_left_inv`, `inv_mul_self` → `inv_mul_cancel` (for `Group`)
    * `mul_right_inv`, `mul_inv_self` → `mul_inv_cancel`
    * `add_left_neg`, `neg_add_self` → `neg_add_cancel` (for `AddGroup`)
    * `add_right_neg`, `add_neg_self` → `add_neg_cancel`
    * `inv_mul_cancel` → `inv_mul_cancel₀` (for `GroupWithZero`)
    * `mul_inv_cancel` → `mul_inv_cancel₀`

commit 9bb9d9e
Author: Tomáš Skřivan <skrivantomas@seznam.cz>
Date:   Mon Aug 12 15:04:33 2024 +0000

    fix(fun_prop):  few bug fixes for fun_prop (#11092)

    Bug fixes
    1. Fix infinite loop triggered by `(by fun_prop : ?m)`
    2. Support for multiple lambda theorems. For example `ContinuousOn` has multiple versions of composition theorem.
    3. Support for special constant lambda theorem. For example `IsLinearMap R fun _ => 0` should be registered as constant lambda theorem
    4. Improved error messages when trying `fun_prop` on non-fun_prop goal
    5. Improved error messages when missing lambda theorems

commit e04c5f0
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 14:21:50 2024 +0000

    feat(Algebra/Homology): signs for the associativity compatibility of the total complex (#15719)

    This PR introduces a typeclass `ComplexShape.Associative` which takes as inputs six complex shapes `c₁`, `c₂`, `c₃`, `c₁₂`, `c₂₃` and `c`, and asserts compatibilities of signs for the associativity of the total complex of a triple complex. It shall also be used in the construction of the associator isomorphism for the tensor product of homological complexes.

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit 43258d6
Merge: e636099 0de4943
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 15:56:11 2024 +0200

    Merge remote-tracking branch 'origin/uncomment_assert_not_exists' into test/merge_assert_up

commit 639e997
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 13:31:36 2024 +0000

    feat(CategoryTheory/Sites): gluing of sections for Mayer-Vietoris squares (#14957)

    Co-authored-by: Markus Himmel <markus@lean-fro.org>

    Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit 46a72de
Author: Yury G. Kudryashov <urkud@urkud.name>
Date:   Mon Aug 12 13:31:34 2024 +0000

    feat(Ergodic): the left action of a group on itself is ergodic (#14596)

commit f9b79d6
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date:   Mon Aug 12 13:06:56 2024 +0000

    chore(SetTheory/Game/PGame): Add note on `NatCast` (#15713)

    I explain that this is not in fact the usual definition for natural numbers as games (a fact that just cost me a few hours of dev time...)

commit 40b6b14
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 13:06:54 2024 +0000

    feat(Algebra/Homology): develop the API for the action of bifunctors on homological complexes (#15712)

commit a83f96c
Author: grhkm21 <grhkm21@gmail.com>
Date:   Mon Aug 12 13:06:52 2024 +0000

    chore: Fix enccard typo in Cardinal file (#15709)

    Fix typo in theorem name

    Moves:
    - Function.Embedding.enccard_le -> Function.Embedding.encard_le

commit 58d29b1
Author: Pim Otte <otte.pim@gmail.com>
Date:   Mon Aug 12 13:06:50 2024 +0000

    feat(Combinatorics/SimpleGraph/Matching): Add matching free graphs (#15357)

    Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

commit ac8cc94
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 13:06:49 2024 +0000

    feat(Algebra/Homology): action of the flip of a bifunctor on homological complexes (#11713)

    We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit b1f62bd
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Mon Aug 12 12:57:15 2024 +0000

    chore: remove unused argument from Behrend.map_injOn (#15735)

commit a9c4c79
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 11:58:20 2024 +0000

    chore: update Mathlib dependencies 2024-08-12 (#15728)

    Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

commit 81b928c
Author: Jakob von Raumer <jakob@von-raumer.de>
Date:   Mon Aug 12 10:18:59 2024 +0000

    feat(CategoryTheory): Equivalence between certain comma categories and products (#15648)

commit 815eabc
Author: Jakob von Raumer <jakob@von-raumer.de>
Date:   Mon Aug 12 10:09:28 2024 +0000

    feat(CategoryTheory): Finality of functors from filtered categories into PUnit (#15641)

commit 0de4943
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 16:52:22 2024 +1000

    move

commit 07189b5
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 16:40:40 2024 +1000

    chore: uncomment some now viable assert_not_exists

…15357)

Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

…15357)

Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

…15357)

Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem