leanprover-community/mathlib

Pull Requests Commits

YaelDillies committed 3 years ago

5aae41f7

Merge remote-tracking branch 'origin/master' into finpartition_index

YaelDillies committed 3 years ago

5a244431

refactor(algebra/ring/basic): rename lemmas about `a*(-b)` and `(-a)*b` (#11925)

eric-wieser committed 3 years ago

3aa5b8a9

feat(data/complex/basic): re-im set product (#11770)

urkud committed 3 years ago

4e17e081

feat(category_theory/pseudoabelian/basic): basic facts and contructions about pseudoabelian categories (#11817)

joelriou committed 3 years ago

78c39752

feat(analysis/normed_space/basic): add lemmas `nnnorm_mul_le` and `nnnorm_pow_succ_le` (#11915)

j-loreaux committed 3 years ago

56db7ed0

feat(topology/algebra/uniform_group): `cauchy_seq.const_mul` and friends (#11917)

ecstatic-morse committed 3 years ago

a3d6b43c

feat(model_theory/substructures): More operations on substructures (#11906)

awainverse committed 3 years ago

4545e31e

chore(*): update to lean 3.39.1c (#11926)

gebner committed 3 years ago

1ae83049

chore(algebra/order/ring): add a few aliases (#11911)

urkud committed 3 years ago

b1269b0d

feat(*): localized `R[X]` notation for `polynomial R` (#11895)

pechersky committed 3 years ago

85d9f218

feat(group_theory/submonoid/operations): prod_le_iff and le_prod_iff, also for groups and modules (#11898)

nomeata committed 3 years ago

59325814

refactor(number_theory/bernoulli_polynomials): improve names (#11805)

oxarbitrage committed 3 years ago

2b68801b

feat(analysis/complex): a few lemmas about `dist` and `conj` (#11913)

urkud committed 3 years ago

1077eb3c

feat(linear_algebra/basis): `basis.map_equiv_fun` (#11888)

jsm28 committed 3 years ago

36d3b688

style(analysis/special_functions/trigonometric/angle): make types of `sin` and `cos` explicit (#11902)

jsm28 committed 3 years ago

f94b0b31

feat(topology/sheaf_condition): connect sheaves on sites and on spaces without has_products (#11706)

alreadydone committed 3 years ago

9ceb3c2a

chore(data/finsupp/basic): generalize comap_mul_action (#11900)

eric-wieser committed 3 years ago

436966c1

feat(algebra/big_operators/basic): add multiset.prod_sum (#11885)

Ruben-VandeVelde committed 3 years ago

7b91f008

feat(analysis/inner_product_space/basic): `orthonormal.map_linear_isometry_equiv` (#11893)

jsm28 committed 3 years ago

02c9d69d

feat(analysis/complex/isometry): `rotation_symm` (#11891)

jsm28 committed 3 years ago

c61ea33b

feat(analysis/complex/circle): `exp_map_circle_neg` (#11889)

jsm28 committed 3 years ago

2364a091

feat(analysis/special_functions/trigonometric/angle): `sin`, `cos` (#11887)

jsm28 committed 3 years ago

99215e3d

feat(analysis/special_functions/trigonometric/angle): `induction_on` (#11886)

jsm28 committed 3 years ago

98ef84ef

feat(data/list): add some lemmas. (#11879)

Ruben-VandeVelde committed 3 years ago

26179ccd

feat(category_theory/limits): is_limit.exists_unique (#11875)

TwoFX committed 3 years ago

dcbb59c4

feat(category_theory/limits): (co)equalizers in the opposite category (#11874)

TwoFX committed 3 years ago

556483f4

feat(data/set/opposite): the opposite of a set (#11860)

TwoFX committed 3 years ago

7a2a5468

feat(order/complete_lattice): infi_le_iff (#11810)

PatrickMassot committed 3 years ago

0354e56f

chore(algebra/monoid_algebra): generalize lift_nc (#11881)

eric-wieser committed 3 years ago

a2f3f55e

Older