leanprover-community/mathlib

Pull Requests Commits

alexjbest committed 4 years ago

e5aea1a8

refactor(measure_theory/measure/hausdorff): change Hausdorff measure definition at 0 (#10859)

sgouezel committed 4 years ago

ee17ab3a

chore(category_theory/monoidal/End): Adding API for monoidal functors into `C ⥤ C` (#10841)

erdOne committed 4 years ago

289ebe58

feat(linear_algebra/determinant): more properties of the determinant of linear maps (#10809)

sgouezel committed 4 years ago

9f1b9bcd

feat(topology/metric/hausdorff_distance): more properties of cthickening (#10808)

sgouezel committed 4 years ago

0d473696

feat(linear_algebra/affine_space/affine_equiv): isomorphism with the units (#10798)

eric-wieser committed 4 years ago

a6179f61

split(data/finset/*): Split `data.finset.card` and `data.finset.fin` off `data.finset.basic` (#10796)

YaelDillies committed 4 years ago

2c4e66f7

feat(linear_algebra/affine_space/combination): vsub distributivity lemmas (#10786)

jsm28 committed 4 years ago

fa46ef10

feat(algebraic_geometry/open_immersion): Easy results about open immersions. (#10776)

erdOne committed 4 years ago

ecec43a2

feat(field_theory/splitting_field): generalize some results from field to domain (#10726)

alexjbest committed 4 years ago

6e59fbe3

feat(order/cover): The covering relation (#10676)

YaelDillies committed 4 years ago

fec084c3

feat(algebra/group/inj_surj): _pow definitions for surjective too (#10832)

eric-wieser committed 4 years ago

011203d9

feat(data/matrix/rank): rank of a matrix (#10826)

jcommelin committed 4 years ago

59152548

feat(linear_algebra/orientation): add orientation.map (#10815)

eric-wieser committed 4 years ago

915e2b5b

feat(ring_theory/prinicipal_ideal_domain): Bézout's lemma for PIDs (#10810)

Ruben-VandeVelde committed 4 years ago

e70faf34

feat(linear_algebra/affine_space/affine_subspace): affine_subspace.comap (#10795)

eric-wieser committed 4 years ago

47c676ed

feat(topology/algebra/mul_action): add an instance in the presence of `is_central_scalar` (#10787)

eric-wieser committed 4 years ago

00454f23

feat(ring_theory/local_properties): Being finite / of finite type is local. (#10775)

erdOne committed 4 years ago

56033982

feat(order): define a `rel_hom_class` for types of relation-preserving maps (#10755)

Vierkantor committed 4 years ago

c10a8728

feat(algebraic_geometry): A scheme is reduced iff its stalks are reduced. (#10879)

erdOne committed 4 years ago

af682d35

feat(analysis/calculus/deriv): add `has_deriv_at.tendsto_punctured_nhds` (#10877)

urkud committed 4 years ago

65118e5f

feat(ring_theory/integral_closure): A subalgebra is contained in the integral closure iff it is integral (#10874)

tb65536 committed 4 years ago

01088844

feat(algebra/algebra/subalgebra): Elements of supremum (#10872)

tb65536 committed 4 years ago

7de517b2

feat(algebra/algebra/subalgebra): Lemmas about `alg_hom.range` (#10871)

tb65536 committed 4 years ago

df113020

feat(algebraic_geometry): The underlying topological space of a Scheme is T0 (#10869)

erdOne committed 4 years ago

ac10136f

feat(data/int): various lemmas (#10862)

Ruben-VandeVelde committed 4 years ago

cb0a6f70

feat(algebra/group/basic): add a few lemmas (#10856)

urkud committed 4 years ago

04e2f5f7

feat(analysis/normed_space/lattice_ordered_group): prove `order_closed_topology` for `normed_lattice_add_comm_group` (#10838)

RemyDegenne committed 4 years ago

5859ec0f

chore(*): more assorted proof simplifications (#10863)

alexjbest committed 4 years ago

6353d6b2

refactor(*): kill a few uses of finish (#10860)

sgouezel committed 4 years ago

0e995a37

Older