leanprover-community/mathlib

Pull Requests Commits

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

feat(data/nat/prime): move nat.prime_iff_prime_int; add int.prime_two/three (#12133)

Ruben-VandeVelde committed 3 years ago

afcc7e74

feat(topology/algebra/{group,monoid}): nat and int scalar multiplication is continuous (#12124)

eric-wieser committed 3 years ago

37019db9

feat(analysis/inner_product_space/projection): norm_sq_eq_sum_norm_sq… (#12096)

hparshall committed 3 years ago

72252b3c

feat(order/filter): prod_assoc (#12002)

PatrickMassot committed 3 years ago

271c3237

feat(group_theory/nilpotent): n-ary products of nilpotent group (#11829)

nomeata committed 3 years ago

d8d2f543

Newer Older