leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/extensive): Add instances of extensive categories (#17495)

erdOne committed 3 years ago

cc858401

feat(topology/algebra/star_subalgebra): add basic theory for topological star subalgebras (#17183)

j-loreaux committed 3 years ago

b7f5a77f

feat(*): update to Lean 3.49 (#17470)

kim-em committed 3 years ago

82a53736

move(group_theory/group_action/*): Move pointwise subgroup operations (#17491)

YaelDillies committed 3 years ago

f86ad885

perf(analysis/complex/circle): fix a slow `@[simps]` (#17504)

j-loreaux committed 3 years ago

ad3dfaca

chore(analysis/convex/strict_convex_space): generalize/add `strict_convex_space.of_*` lemmas (#17206)

urkud committed 3 years ago

c749cc93

feat(linear_algebra/{basic, affine_space/restrict}): better support for restriction of affine and linear maps (#16397)

datokrat committed 3 years ago

f0f3d964

feat(topology/metric_space/hausdorff_distance): The diameter of a thickening (#17021)

YaelDillies committed 3 years ago

08aeb33b

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

leanprover-community-bot committed 3 years ago

d240ffbd

chore(ring_theory): split `ring_theory.algebra_tower` (#17480)

Vierkantor committed 3 years ago

f4bce070

chore(linear_algebra): remove `finite_dimensional` import from `finsupp_vector_space` (#17474)

Vierkantor committed 3 years ago

019ead10

feat(group_theory/group_action/defs): `is_central_vadd` (#17446)

YaelDillies committed 3 years ago

2efabeb7

feat(ring_theory/is_tensor_product): Add predicate `algebra.is_pushout`. (#17197)

erdOne committed 3 years ago

825b341b

perf(ring_theory/polynomial/bernstein): fix timeout (#17484)

astrainfinita committed 3 years ago

bb5be046

chore(data/quot): freeze (#17479)

Vierkantor committed 3 years ago

d337708d

feat(analysis/inner_product_space): ext lemmas for dense subspaces (#17450)

mcdoll committed 3 years ago

f435f954

feat(algebraic_topology/dold_kan): P_infty vanishes on degeneracies (#17191)

joelriou committed 3 years ago

b12099d3

feat(algebraic_geometry/open_immersion): API for `Scheme.restrict_functor`. (#17184)

erdOne committed 3 years ago

5182bbae

feat(order/basic): Product of dense orders (#17168)

YaelDillies committed 3 years ago

50a4565f

feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum (#17069)

Vierkantor committed 3 years ago

398f60f6

refactor(order/bounded_order): relax typeclass requirements on `disjoint` and `codisjoint` (#16434)

eric-wieser committed 3 years ago

6ca1a09b

feat(group_theory/index): Add typeclass for `finite_index` (#17139)

tb65536 committed 3 years ago

50d3d5f4

feat(measure_theory/measure/measure_space): `volume_preimage_coe` (#17030)

alexjbest committed 3 years ago

e25981a8

chore(linear_algebra): split `finrank` results that don't depend on `finite_dimensional` (#17473)

Vierkantor committed 3 years ago

667de7b2

chore(algebra/ne_zero): freeze (#17475)

mcdoll committed 3 years ago

4ea7cf65

feat(linear_algebra/affine_space/midpoint): `midpoint_vsub`, `vsub_midpoint` (#17278)

jsm28 committed 3 years ago

e3968f66

feat(geometry/euclidean/angle/oriented): more sign lemmas (#17270)

jsm28 committed 3 years ago

878c6289

feat(analysis/special_functions/trigonometric/angle): `tan` (#17268)

jsm28 committed 3 years ago

ec68c3c6

feat(linear_algebra/affine_space/affine_subspace): notation for lines (#17094)

jsm28 committed 3 years ago

beee53c9

feat(linear_algebra/finsupp): add lemmas to deal with `span (range v)`. (#17441)

Jon Eugster committed 3 years ago

e2edca2d

Newer Older