leanprover-community/mathlib3

Pull Requests Commits

urkud committed 4 years ago

a55273fb

feat(algebra/algebra/subalgebra): `subalgebra.map` commutes with supremum (#10899)

tb65536 committed 4 years ago

5dd35377

feat(ring_theory/tensor_product): The tensor product `A ⊗ B` is generated by tensors `a ⊗ₜ b` (#10900)

tb65536 committed 4 years ago

41ced1ca

feat(order/monotone): add `monotone_int_of_le_succ` etc (#10895)

urkud committed 4 years ago

194bde8f

feat(data/list/sort): subperm sorted implies sublist (#10892)

b-mehta committed 4 years ago

a60ef7c9

feat (order/lexicographic): add API lemmas (#10887)

MantasBaksys committed 4 years ago

faee3582

chore(order/complete_lattice): eliminate `finish` (#10876)

stuart-presnell committed 4 years ago

45ed9ded

feat(data/list/count): add lemma `list.count_singleton'` (#10880)

stuart-presnell committed 4 years ago

68d9b42b

feat(algebra/group_power/basic): generalize `zpow_neg_one` to `div_inv_monoid` (#10894)

urkud committed 4 years ago

9e5cbc12

feat(analysis/asymptotics): add `is_O.inv_rev`, `is_o.inv_rev` (#10896)

urkud committed 4 years ago

3fc32e3e

chore(algebra/iterate_hom): use to_additive to fill missing lemmas (#10886)

eric-wieser committed 4 years ago

72224634

chore(scripts): update nolints.txt (#10893)

leanprover-community-bot committed 4 years ago

a2c3b293

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

Older