leanprover-community/mathlib3

Pull Requests Commits

untested changes

eric-wieser committed 2 years ago

a5cd4c92

eric-wieser committed 2 years ago

9bed7232

eric-wieser committed 2 years ago

b9989324

automated replacements

eric-wieser committed 2 years ago

7a743162

eric-wieser committed 2 years ago

a6943083

eric-wieser committed 2 years ago

c98333f3

normed_space fixes

eric-wieser committed 2 years ago

f935866a

eric-wieser committed 2 years ago

342bf4d1

eric-wieser committed 2 years ago

a466c033

refactor(analysis/normed/group/basic): unbundle algebra from norm structure

eric-wieser committed 2 years ago

3d1dde9c

doc(algebra/continued_fractions/*): TeXify docstrings (#18459)

MichaelStollBayreuth committed 2 years ago

2738d2ca

fix(ring_theory/derivation): speed up a slow definition (#18457)

eric-wieser committed 2 years ago

0324bd3f

feat(measure_theory/integral): break up integrals into sums (#18425)

loefflerd committed 2 years ago

e7286cac

ci(.github/workflows): lint for formatting issues in references.bib (#16614)

Ruben-VandeVelde committed 2 years ago

973ed779

fix(.github/workflows): try a fix for review bodies (#18455)

alexjbest committed 2 years ago

1df9a174

feat(topology/algebra/order/upper_lower): The closure of an upper set (#16975)

YaelDillies committed 2 years ago

4330aae2

feat(algebra/order): Unions of interval translates by ℤ (#18427)

loefflerd committed 2 years ago

740acc0e

chore(linear_algebra/dual): prove a lemma with rfl (#18444)

eric-wieser committed 2 years ago

5455cb0b

feat(algebra/continued_fractions/*): add some API lemmas (#18434)

MichaelStollBayreuth committed 2 years ago

10d88727

feat(algebra/algebra/operations): the semiring of submodules over an algebra is idempotent (#18400)

eric-wieser committed 2 years ago

2bbc7e38

feat(combinatorics/simple_graph/connectivity): `concat` and `concat_rec` (#17209)

kmill committed 2 years ago

13cd3e89

feat(algebra/order/field/basic): `a ≤ b / c → a * c ≤ b` (#18367)

YaelDillies committed 2 years ago

5a82b067

split(topology/algebra/infinite_sum): Split into four files (#18414)

YaelDillies committed 2 years ago

32253a1a

chore(set_theory/ordinal/arithmetic): move power and logarithm to a new file (#18441)

eric-wieser committed 2 years ago

f1e061e3

feat (analysis/special_functions): limit formula and reflection formula for Gamma (#18404)

loefflerd committed 2 years ago

372edc36

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

leanprover-community-bot committed 2 years ago

1ead2234

chore(algebra/group/units): is_add_unit.decidable (#18439)

pechersky committed 2 years ago

369525b7

feat(analysis/fourier): Basic framework for Fourier transforms (#18428)

loefflerd committed 2 years ago

a231f964

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

leanprover-community-bot committed 2 years ago

ac34df03

refactor(combinatorics/configuration): Refactor `projective_plane` to extend `has_points` and `has_lines` (#18436)

tb65536 committed 2 years ago

26c71658

Newer Older