leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 3 years ago

972a949f

Merge remote-tracking branch 'origin/master' into geometric-group-theory

YaelDillies committed 3 years ago

976b775f

YaelDillies committed 3 years ago

87516e7d

chore(.github/CODEOWNERS): two new rules (#16921)

jcommelin committed 3 years ago

b49d5686

feat(group_theory/transfer): The kernel of the transfer homomorphism `G →* P` is disjoint from every `p`-group (#16914)

tb65536 committed 3 years ago

6979111c

refactor(set_theory/cardinal): review API about `#α = 2`/`nat.card α = 2` (#16899)

urkud committed 3 years ago

73ccd02e

feat(combinatorics/quiver/path): Composition is injective (#16852)

YaelDillies committed 3 years ago

98c944e9

feat(topology/algebra/infinite_sum): infinite sums on subsets (#16671)

fpvandoorn committed 3 years ago

6ef05bb3

feat(topology/basic): add `is_closed.interior_union` and `is_closed.interior_union'` (#16599)

astrainfinita committed 3 years ago

5ef85df4

feat(order/well_founded, data/fin/tuple/*, ...): add `well_founded.induction_bot`, `tuple.bubble_sort_induction` (#16536)

MichaelStollBayreuth committed 3 years ago

6e4c1b31

feat(linear_algebra/matrix): Schur complement (#15270)

abentkamp committed 3 years ago

68ead6e6

feat(linear_algebra/affine_space/finite_dimensional): `coplanar` (#16910)

jsm28 committed 3 years ago

4d5491dc

feat(geometry/euclidean/oriented_angle): signs of angles and `same_ray` (#16909)

jsm28 committed 3 years ago

b30449d6

feat(algebraic_geometry/prime_spectrum/maximal): maximal spectrum (#16905)

Multramate committed 3 years ago

12edc988

feat(category_theory/localization): developing the predicate is_localization (#16890)

joelriou committed 3 years ago

032f11f8

feat(analysis/inner_product_space/orientation): volume form (#16487)

hrmacbeth committed 3 years ago

265fe3d8

feat(group_theory/subgroup/basic): add some trivial lemmas (#16915)

urkud committed 3 years ago

01788b5e

feat(algebra/order/sub): add tsub_tsub_tsub_cancel_left (#16887)

mariainesdff committed 3 years ago

5b4d38a2

refactor(measure_theory/group/prod): rename the variables (#16707)

fpvandoorn committed 3 years ago

59de3c16

feat(polynomial/degree/trailing_degree): redefine `trailing_degree` as `p.support.min` (#16337)

astrainfinita committed 3 years ago

cbaea5dd

feat(category_theory/sites): Surjective presheaf morphisms. (#15283)

erdOne committed 3 years ago

2c882621

feat(measure_theory/integral/periodic): relate integrals over `add_circle` with integrals upstairs in `ℝ` (#16836)

hrmacbeth committed 3 years ago

f1138dc3

feat(topology/sets/closeds): atoms in a t1_space are singletons (#16721)

j-loreaux committed 3 years ago

2e348d40

chore(analysis/calculus/diff_ont_int_cont): rename to diff_cont_on_cl to match content (#16908)

sgouezel committed 3 years ago

8e9df645

feat(data/finset/basic): add instance `is_empty ↥∅` (#16902)

alreadydone committed 3 years ago

43a6243f

fix(number_theory/cyclotomic/basic): change variable names, fix doc (#16901)

jcommelin committed 3 years ago

ea3dac31

refactor(archive/100-theorems-list/02_cubing_a_cube): review API (#16898)

urkud committed 3 years ago

113568c9

feat(data/option/basic): add `option.{forall,exists}_mem_map` (#16897)

urkud committed 3 years ago

c5549d56

chore(*): remove uses of with_cases (#16894)

alexjbest committed 3 years ago

4d416710

feat(category_theory): yoneda functor on abelian category preserves finite colimits iff object is injective (#16893)

javra committed 3 years ago

8853975e

Older