leanprover-community/mathlib

Pull Requests Commits

bottine committed 2 years ago

6e1a4d55

make #lint happy

bottine committed 2 years ago

8eb596e7

Integrate changes from #18410

0art0 committed 2 years ago

7eef3fd4

Enclose definitions in the `connected_component` namespace

0art0 committed 2 years ago

c6819dec

Incorporate changes from #18410

0art0 committed 2 years ago

a493a214

Merge branch 'master' into 0art0/simple_graph/component.supp

0art0 committed 2 years ago

Verified f07c076b

Restore deleted lemma

0art0 committed 2 years ago

82a5baba

Update src/combinatorics/simple_graph/connectivity.lean

0art0 committed 2 years ago

Verified da1d33d8

Update src/combinatorics/simple_graph/connectivity.lean

0art0 committed 2 years ago

Verified 482b617c

Remove `subgraph_of_adj_connected`

0art0 committed 2 years ago

202c8208

Changes to `connected_component.iso_equiv_supp`

0art0 committed 2 years ago

5ee90a9a

Adjust `connected_component_mk_mem`

0art0 committed 2 years ago

9219a165

Fix `supp_injective`

0art0 committed 2 years ago

ba4e22fa

0art0 committed 2 years ago

6130123e

Adjust `iso_image_comp_eq_map_iff_eq_comp`

0art0 committed 2 years ago

e9703322

Adjust `mk_eq_of_adj`

0art0 committed 2 years ago

177215b7

Golf `iso.symm_apply_reachable` proof

0art0 committed 2 years ago

c3967eb5

Remove `connected_component.connected`

0art0 committed 2 years ago

84fc0a81

doc(order/game_add): minor doc improvement (#18525)

vihdzp committed 2 years ago

fee218fb

chore(ring_theory/polynomial): squeeze a `simpa` (#18524)

Vierkantor committed 2 years ago

dfb0adb7

doc(set_theory/ordinal/exponential): improve module docstring (#18522)

vihdzp committed 2 years ago

8ee653c0

feat(analysis/convex/extreme): Extreme points of `s ×ˢ t` (#18171)

YaelDillies committed 2 years ago

c5773405

chore(combinatorics/simple_graph/connectivity): open a namespace block for `connected_component` (#18520)

bottine committed 2 years ago

e876965f

fix(algebra/star/star_alg_hom): fix typo in `star_alg_hom.coe_coe` (#18519)

j-loreaux committed 2 years ago

35882ddc

feat(combinatorics/simple_graph/basic): Simple graphs form a complete boolean algebra (#18285)

YaelDillies committed 2 years ago

c6ef6387

chore(*): add mathlib4 synchronization comments (#18494)

leanprover-community-bot committed 2 years ago

ee05e9ce

refactor(category theory/cofiltered_systems): rename `mittag_leffler.lean` and move `nonempty_sections_of_fintype_cofiltered_system` into new file (#18433)

bottine committed 2 years ago

8195826f

feat(combinatorics/simple_graph/regularity/bound): Local `positivity` extension (#18368)

YaelDillies committed 2 years ago

7a0dd7b2

chore(set_theory/ordinal/fixed_point): style + comments (#18322)

vihdzp committed 2 years ago

0dd4319a

refactor(ring_theory): submodules that are units are finitely generated (#18510)

alreadydone committed 2 years ago

ed90a7d3

Older