leanprover-community/mathlib3

Pull Requests Commits

alreadydone committed 2 years ago

2553b2ed

fix incomplete docstring

alreadydone committed 2 years ago

36e9a968

import field_theory.galois seems to do nothing now

alreadydone committed 2 years ago

be363c50

@[simp] to_class_some makes simp_nf linter fail

alreadydone committed 2 years ago

7d4097e6

partial cleanup

alreadydone committed 2 years ago

3951772b

Remove redundant assumption

Multramate committed 2 years ago

ea162c8c

Merge branch 'master' into associativity

Multramate committed 2 years ago

1c47099c

feat(algebraic_geometry/elliptic_curve/point): define addition of K-rational points (#17194)

Multramate committed 2 years ago

67f92b6f

feat(measure_theory/group.measure): add pi.is_haar_measure (#18390)

xroblot committed 2 years ago

4b83fd28

chore(measure_theory/decomposition/unsigned_hahn): speedup Hahn decomposition (#18419)

sgouezel committed 2 years ago

0f1becb7

chore(algebra/quaternion): missing trivial lemmas (#18413)

eric-wieser committed 2 years ago

d3e3adc9

feat(analysis/fourier): Riemann-Lebesgue lemma (part 1) (#18361)

loefflerd committed 2 years ago

735b22f8

chore(topology/algebra): make the divisor argument of `div_const` explicit (#18411)

eric-wieser committed 2 years ago

8c8c544b

refactor(topology/sets/opens): use a `structure` for `opens` and `open_nhds_of` (#18409)

urkud committed 2 years ago

d39590fc

chore(topology/constructions): pi.single is continuous (#18412)

eric-wieser committed 2 years ago

dde670c9

feat(analysis/quaternion): add `complete_space`, `module.free`, and `module.finite` instances (#18347)

eric-wieser committed 2 years ago

24f7dbdf

feat(measure_theory/integral/set_integral): remove or weaken some integrability assumptions (#18395)

sgouezel committed 2 years ago

a7589864

feat(analysis/special_functions/trigonometric/series): express `cos`/`sin` as infinite sums (#18352)

eric-wieser committed 2 years ago

ccf84e0d

chore(*): remove default.lean files that had nothing but imports (#18408)

urkud committed 2 years ago

916aaa16

chore(topology/algebra/infinite_sum): correct argument explicitness (#18403)

eric-wieser committed 2 years ago

639b66d9

chore(*): add mathlib4 synchronization comments (#18406)

leanprover-community-bot committed 2 years ago

b6da1a0b

chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402)

eric-wieser committed 2 years ago

38d38e09

feat (analysis/special_functions): add the Beta function (#18373)

loefflerd committed 2 years ago

c8fc41b2

feat(topology/algebra/infinite_sum): add tsum_finset_bUnion_disjoint (#18350)

eric-wieser committed 2 years ago

cd424234

refactor(topology/discrete_quotient): review API (#18401)

urkud committed 2 years ago

d101e931

feat(combinatorics/simple_graph/ends): Definition (only) of the ends of a simple_graph. (#17857)

bottine committed 2 years ago

db53863f

feat(logic/equiv/fin): `div`/`mod` as an equivalence on `nat`/`int` (#18359)

eric-wieser committed 2 years ago

bd835ef5

feat(combinatorics/catalan): Connection between Catalan numbers and number of trees (#16583)

prakol16 committed 2 years ago

26b40791

feat(analysis/complex/basic): lemmas about tsum (#18376)

eric-wieser committed 2 years ago

2407f3b1

doc(topology/uniform_space/abstract_completion): typo (#18399)

mcdoll committed 2 years ago

69966de7

Older