Commits leanprover-community/mathlib3

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

Define equivalence between height one and maximal spectra for one-dimensional rings

Multramate committed 3 years ago

95d651d6

Apply name changes and remove redundant instances

Multramate committed 3 years ago

da9b530b

Revert name changes

Multramate committed 3 years ago

2fe88951

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

feat(algebraic_topology/dold_kan): very basic defs for split simplicial objects in preadditive categories (#16888)

joelriou committed 3 years ago

24f5150e

feat(ring_theory/ideal/local_ring): add local_ring.residue_field.map_id & local_ring.residue_field.map_comp (#16916)

mkaratarakis committed 3 years ago

bbcc67f5

feat(logic/equiv/transfer_instances, group_theory/eckmann_hilton): make definitions reducible (#16884)

alreadydone committed 3 years ago

2f93d81c

feat(topology/uniform_space): local uniform convergence on union (#16883)

b-mehta committed 3 years ago

a4efbb0e

feat(logic/basic): add four lemmas about (d)ite (#16879)

alreadydone committed 3 years ago

5fd24816

feat(data/real/ereal): `coe : ℝ → ereal` is strictly monotone (#16607)

YaelDillies committed 3 years ago

7507876b