leanprover-community/mathlib

Pull Requests Commits

typo in W/basic

Jlh18 committed 3 years ago

3a779fa3

insts of W, initl algs, W as init alg, poly funcs

Jlh18 committed 3 years ago

50f9a115

feat(topology/support): define topological support and compactly supported functions (#11923)

fpvandoorn committed 3 years ago

8413f078

feat(order/hom/lattice): Finitary join-/meet-preserving maps (#12149)

YaelDillies committed 3 years ago

80591d65

refactor(topology/*): Hom classes for continuous maps/homs (#11909)

YaelDillies committed 3 years ago

68efb10c

feat(analysis/seminorm): add inf (#11791)

pbazin committed 3 years ago

247943a9

chore(algebra/lie/engel): speed up proof of Engel's theorem slightly (#12205)

ocfnash committed 3 years ago

9a7ed8cb

feat(category_theory/limits): is_bilimit (#12108)

TwoFX committed 3 years ago

cb45da26

feat(analysis/specific_limits): dirichlet and alternating series tests (#11908)

ecstatic-morse committed 3 years ago

e16e093e

perf(geometry/euclidean): speed up proof on the edge of timing out (#12191)

robertylewis committed 3 years ago

d77e91f8

feat(analysis/normed_space/basic): `norm_matrix_lt_iff` (#12151)

hparshall committed 3 years ago

22464cf6

feat(measure_theory/integral/set_integral): Bochner integral with respect to a measure with density (#12123)

sgouezel committed 3 years ago

eb5c5ed5

feat(tactic/linear_combination): improve error messages and degenerate case (#12062)

robertylewis committed 3 years ago

8aa26b27

feat(algebra/star/self_adjoint): remove commutativity hypothesis from `has_pow (self_adjoint R)` (#12188)

j-loreaux committed 3 years ago

2971f3dc

feat(category_theory/equivalence): if two functors F and G are isomorphic, F is an equivalence iff G is (#12162)

joelriou committed 3 years ago

a6078202

feat(analysis/normed_space/basic): `norm_entry_le_entrywise_sup_norm` (#12159)

hparshall committed 3 years ago

9a17b556

feat(algebra/ring/ulift): add a `field` instance (#12141)

ericrbg committed 3 years ago

1cfbcc63

feat(analysis/inner_product_space/spectrum): `pos_nonneg_eigenvalues` (#12161)

hparshall committed 3 years ago

e3d36811

feat(probability/stopping): filtrations are a complete lattice (#12169)

RemyDegenne committed 3 years ago

02dc6f25

refactor(*): move normed field lemmas into root namespace (#12163)

j-loreaux committed 3 years ago

9ed71796

feat(geometry/euclidean/oriented_angle): oriented angles and rotations (#12106)

jsm28 committed 3 years ago

95d22b52

feat(category_theory/preadditive): separators in preadditive categories (#11884)

TwoFX committed 3 years ago

6db15773

chore(topology/algebra/infinite_sum): reference Cauchy criterion in docs (#12172)

ecstatic-morse committed 3 years ago

3ad73951

feat(order/*): Missing order lifting instances (#12154)

YaelDillies committed 3 years ago

634dfc8a

feat(group_theory/free_product): is_free_group_free_product_of_is_free_group (#12125)

nomeata committed 3 years ago

2f33463f

doc(topology/dense_embedding): fix markdown (#12180)

eric-wieser committed 3 years ago

7c6678ad

chore(data/set/basic): add a few lemmas and a `@[simp]` attribute (#12176)

urkud committed 3 years ago

f66a5ddb

feat(topology/algebra): if a subobject is commutative, then so is its topological closure (#12170)

dupuisf committed 3 years ago

0eb5e2d1

feat(category_theory/opposites): nat_trans.remove_unop (#12147)

TwoFX committed 3 years ago

56dbb604

chore(data/nat/prime): slightly golf proof of mem_factors (#12143)

Ruben-VandeVelde committed 3 years ago

b3b5e355

Older