leanprover-community/mathlib

Pull Requests Commits

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

feat(geometry/euclidean/angle/oriented/basic): `inner_eq_zero` lemmas (#17265)

jsm28 committed 3 years ago

34d8782b

feat(geometry/euclidean/angle/oriented/affine): signs of angles and sides of subspaces (#17234)

jsm28 committed 3 years ago

35ca0862

feat(group_theory/transfer): Prove Burnside's transfer theorem (#17263)

tb65536 committed 3 years ago

d3731988

chore(ring_theory/ideal/local_ring): use `derive` for more consistent instances (#17468)

eric-wieser committed 3 years ago

d1accf4f

feat(topology/algebra/module/finite_dimension): add `linear_map.is_open_map_of_finite_dimensional` (#17466)

urkud committed 3 years ago

c6c8f200

doc(undergrad.yaml): representation theory (#17459)

antoinelab01 committed 3 years ago

c005eac4

doc(overview.yaml): representation theory (#17458)

antoinelab01 committed 3 years ago

8d9f31db

feat(group_theory/order_of_element): lemmas about orders of powers of group elements (#17433)

ocfnash committed 3 years ago

ac825bfa

chore(data/nat/prime): add 2 aliases (#17372)

urkud committed 3 years ago

c946d609

feat(linear_algebra/dual): more about `dual_annihilator` (#17313)

kmill committed 3 years ago

c9b80414

feat(ring_theory/dedekind_domain): lemmas on inequality between ideal powers (#17188)

Vierkantor committed 3 years ago

20c144b5

feat(analysis/normed{_space/basic, /field/basic}): add some induced norm structures on subobjects (#17169)

j-loreaux committed 3 years ago

089f741b

feat(group_theory/submonoid/membership): +2 induction principles (#17160)

urkud committed 3 years ago

95e5153a

feat(algebra/ring/equiv): add lemma on coercion to equivs and symm (#17101)

alexjbest committed 3 years ago

642809e9

Newer Older