leanprover-community/mathlib

Pull Requests Commits

chore(data/finset/pointwise): `{a} • t = a • t` (#17072)

YaelDillies committed 3 years ago

a2a19634

feat(topology/metric_space/basic): Distance between constant functions (#16958)

YaelDillies committed 3 years ago

3798ca1d

feat(order/directed): A few more lemmas (#16953)

YaelDillies committed 3 years ago

34826f0d

chore(order/filter/*): golf `ultrafilter.exists_ultrafilter_of_finite_inter_nonempty` (#17096)

urkud committed 3 years ago

3fbddc20

feat(category_theory/morphism_property): Define `morphism_property.universally`. (#17112)

erdOne committed 3 years ago

7dff92aa

feat(topology/continuous_on): Continuity on an open (#17089)

YaelDillies committed 3 years ago

54349530

chore(data/nat/enat): move into a subfolder (#17106)

urkud committed 3 years ago

8005d575

chore(data/set/basic): reflow/golf some proofs (#17066)

urkud committed 3 years ago

5bff97f2

chore(analysis/calculus/lhopital): use the new `nhds_within` notation (#17099)

eric-wieser committed 3 years ago

76c3f725

perf(analysis/normed_space/lp_space): fix timeout by squeezing simps (#17108)

alreadydone committed 3 years ago

a1c17e2a

feat(topology/covering): Define covering spaces (#16087)

tb65536 committed 3 years ago

42d514e8

refactor(analysis/special_functions/trigonometric/inverse): `cos_arcsin`, `sin_arccos` degenerate cases (#17026)

jsm28 committed 3 years ago

b1a619c0

feat(representation_theory/group_cohomology_resolution): add exactness properties of resolution (#17005)

Amelia Livingston committed 3 years ago

618ea3d5

feat(analysis/inner_product_space/basic): Pythagoras with square roots (#17025)

jsm28 committed 3 years ago

b5dd709b

feat(analysis/special_functions/trigonometric/basic): `tan_pi_div_two_sub` (#17024)

jsm28 committed 3 years ago

d94370d1

feat(algebra|data): misc lemmas in low-level files (#16948)

fpvandoorn committed 3 years ago

86b9ee4e

feat(data/matrix/pequiv): Added `to_pequiv_matrix_mul` (#16732)

jreaso committed 3 years ago

3793e329

feat(ring_theory/localization/fraction_ring): add coe_inj (#17087)

kbuzzard committed 3 years ago

24586ea0

fix(analysis/normed_space/lp_space): speedup by squeezing simps (#17098)

sgouezel committed 3 years ago

2a2e7ae6

chore(category_theory/concrete_category): remove imports (#17093)

kim-em committed 3 years ago

6c6597fa

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

leanprover-community-bot committed 3 years ago

d5aabe16

feat(algebra/ring/equiv): Add `ring_equiv.comp_symm` (#17045)

mkaratarakis committed 3 years ago

ee5e5e82

chore(scripts/port_status.py): support code-blocked yaml (#17076)

pechersky committed 3 years ago

ea1362f2

chore(algebra/squarefree): rename `squarefree_of_dvd_of_squarefree` for dot notation (#17071)

alexjbest committed 3 years ago

f5138420

feat(measure_theory/integral/interval_integral): add lemmas (#16986)

fpvandoorn committed 3 years ago

c99203f7

feat(analysis/inner_product_space/two_dim): the case of `ℂ` (#16929)

hrmacbeth committed 3 years ago

bdcb5fb7

chore: freeze `data.bracket` (#17077)

javra committed 3 years ago

eed79d6e

chore: update scripts/port_status for more flexible tagging (#17056)

kim-em committed 3 years ago

0578d23f

chore(algebra/*): mark frozen files that have been ported to mathlib4 (#17039)

kim-em committed 3 years ago

97bdf517

chore(logic/basic): add move eq_true from core, as eq_true_iff (#17060)

kim-em committed 3 years ago

4aa2a2e1

Newer Older