leanprover-community/mathlib

Pull Requests Commits

refactor(linear_algebra/bilinear_map): move lemmas about `basis` to a new file. (#18468)

eric-wieser committed 3 years ago

87c54600

feat(data/prod): bijectivity of prod.map (#18446)

eric-wieser committed 3 years ago

bd9851ca

chore(linear_algebra/prod): add a missing lemma (#18445)

eric-wieser committed 3 years ago

57a30493

chore(number_theory/sum_four_squares): squeeze simps (#18467)

eric-wieser committed 3 years ago

f434b205

feat(probability/kernel/basic): add kernel.with_density (#18463)

RemyDegenne committed 3 years ago

31a8a276

feat(algebra/quandle): Unital shelves (#17839)

kisonecat committed 3 years ago

28aa996f

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

github-actions[bot] committed 3 years ago

e97cf15c

chore(number_theory/sum_four_squares): squeeze simps (#18461)

eric-wieser committed 3 years ago

297619ec

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

MichaelStollBayreuth committed 3 years ago

2738d2ca

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

eric-wieser committed 3 years ago

0324bd3f

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

loefflerd committed 3 years ago

e7286cac

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

Ruben-VandeVelde committed 3 years ago

973ed779

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

alexjbest committed 3 years ago

1df9a174

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

YaelDillies committed 3 years ago

4330aae2

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

loefflerd committed 3 years ago

740acc0e

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

eric-wieser committed 3 years ago

5455cb0b

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

MichaelStollBayreuth committed 3 years ago

10d88727

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

eric-wieser committed 3 years ago

2bbc7e38

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

kmill committed 3 years ago

13cd3e89

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

YaelDillies committed 3 years ago

5a82b067

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

YaelDillies committed 3 years ago

32253a1a

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

eric-wieser committed 3 years ago

f1e061e3

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

loefflerd committed 3 years ago

372edc36

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

github-actions[bot] committed 3 years ago

1ead2234

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

pechersky committed 3 years ago

369525b7

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

loefflerd committed 3 years ago

a231f964

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

github-actions[bot] committed 3 years ago

ac34df03

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

tb65536 committed 3 years ago

26c71658

chore(algebra/quaternion): generalize the algebra instance (#18382)

eric-wieser committed 3 years ago

48085f14

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

github-actions[bot] committed 3 years ago

34ee86e6

Newer Older