leanprover-community/mathlib3

Pull Requests Commits

n-ary cauchy products

eric-wieser committed 3 years ago

236f92f8

feat(data/fin/tuple/nat_antidiagonal): add trivial equiv

eric-wieser committed 3 years ago

3dc21700

eric-wieser committed 3 years ago

52c72aa5

Merge branch 'master' into eric-wieser/antidiagonal_tuple

eric-wieser committed 3 years ago

Verified 2b1f7e5e

chore(topology/algebra/infinite_sum): weaken from equiv to surjective (#13164)

eric-wieser committed 3 years ago

429c6e35

chore(model_theory/basic): Fix namespace on notation for first-order maps (#13145)

awainverse committed 3 years ago

4c83474d

chore(data/fin/tuple/basic): lemmas about `cons` (#13027)

eric-wieser committed 3 years ago

41cd2f82

chore(order/complete_lattice): Generalize `⨆`/`⨅` lemmas to dependent families (#13154)

YaelDillies committed 3 years ago

4eee8bc3

chore(number_theory/cyclotomic/discriminant): golf `repr_pow_is_integral` a little (#13167)

alexjbest committed 3 years ago

bae79d04

chore(topology/algebra/module/basic): add continuous_linear_map.copy (#13166)

eric-wieser committed 3 years ago

a925d1dd

chore(order/*): generalisation linter (#13105)

kim-em committed 3 years ago

05e2fc02

feat(group_theory/torsion): define torsion subgroups and show they're torsion (#12769)

Julian committed 3 years ago

fe21f5de

refactor(order/succ_order/basic): Use `is_min`/`is_max` (#12597)

YaelDillies committed 3 years ago

21082848

feat(order/filter/n_ary): Binary and ternary maps of filters (#13062)

YaelDillies committed 3 years ago

f55d3524

feat(algebra/big_operators): add `commute.*_sum_{left,right}` lemmas (#13035)

eric-wieser committed 3 years ago

b189be76

refactor(group_theory/schur_zassenhaus): Some golfing (#13017)

tb65536 committed 3 years ago

19448a93

chore(measure_theory/function/locally_integrable): fix typo (#13160)

sgouezel committed 3 years ago

0cb9407a

feat(algebra/quaternion): Cardinality of quaternion algebras (#12891)

vihdzp committed 3 years ago

6dde651a

feat(number_theory/cyclotomic/discriminant): add discr_zeta_eq_discr_zeta_sub_one (#12710)

riccardobrasca committed 3 years ago

8cb151f7

fix(data/polynomial/basic): op_ring_equiv docstring (#13132)

kbuzzard committed 3 years ago

61e18ae1

feat(topology/uniform_space/basic): constructing a `uniform_space.core` from a filter basis for the uniformity (#13065)

ADedecker committed 3 years ago

36e1cdf8

feat(category_theory/abelian): transferring "abelian-ness" across a functor (#13059)

kim-em committed 3 years ago

12128187

feat(analysis/special_functions): add the Gamma function (#12917)

loefflerd committed 3 years ago

6e26cff9

chore(*): Bump to Lean 3.42.1 (#13146)

PatrickMassot committed 3 years ago

6e5ca7d0

docs(data/polynomial/basic): Remove commutative from doc-module (#13144)

adomani committed 3 years ago

d6731a48

chore(topology/vector_bundle): split long proof (#13142)

hrmacbeth committed 3 years ago

4f14d4d4

feat(logic/small, model_theory/*): Smallness of vectors, lists, terms, and substructures (#13123)

awainverse committed 3 years ago

410e3d0e

chore(algebra/*): generalisation linter (#13109)

kim-em committed 3 years ago

2d22b5d3

chore(ring_theory/polynomial/pochhammer): make semiring implicit in a lemma that I just moved (#13077)

adomani committed 3 years ago

d33ea7b2

feat(logic/function/basic): add some more API for `injective2` (#13074)

eric-wieser committed 3 years ago

955e95ad

Older