leanprover-community/mathlib

Pull Requests Commits

refactor(topology/algebra/mul_action2): rename type classes (#11940)

urkud committed 4 years ago

ea0e4589

feat(order/hom/bounded): Bounded order homomorphisms (#11806)

YaelDillies committed 4 years ago

4e8d8faa

doc(algebra/group/hom_instances): Fix spellings (#11943)

mans0954 committed 4 years ago

46911598

feat(topology/uniform_space/cauchy): add a few lemmas (#11912)

urkud committed 4 years ago

352e0642

feat(topology): a few more results about compact sets (#11905)

fpvandoorn committed 4 years ago

2b9aca75

feat(set_theory/ordinal_arithmetic): `le_one_iff` (#11847)

vihdzp committed 4 years ago

b8fb8e5b

feat(algebra.group.hom_instances): Define left and right multiplication operators (#11843)

mans0954 committed 4 years ago

2726e238

feat(order): some properties about monotone predicates (#11904)

fpvandoorn committed 4 years ago

5008de8b

feat(order/filter/basic): add lemma `le_prod_map_fst_snd` (#11901)

berndlosert committed 4 years ago

d3cdcd83

chore(data/pi): add pi.prod and use elsewhere (#11877)

eric-wieser committed 4 years ago

9648ce29

feat(order/atoms): finite orders are (co)atomic (#11930)

nomeata committed 4 years ago

ca2450fe

chore(algebra/tropical/basic): remove 3 instances (#11920)

adomani committed 4 years ago

c8827532

chore(data/fintype/basic): documenting elaboration bug (#11247)

kmill committed 4 years ago

fea68aac

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

eric-wieser committed 4 years ago

3aa5b8a9

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

urkud committed 4 years ago

4e17e081

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

joelriou committed 4 years ago

78c39752

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

j-loreaux committed 4 years ago

56db7ed0

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

ecstatic-morse committed 4 years ago

a3d6b43c

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

awainverse committed 4 years ago

4545e31e

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

gebner committed 4 years ago

1ae83049

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

urkud committed 4 years ago

b1269b0d

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

pechersky committed 4 years ago

85d9f218

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

nomeata committed 4 years ago

59325814

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

oxarbitrage committed 4 years ago

2b68801b

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

urkud committed 4 years ago

1077eb3c

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

jsm28 committed 4 years ago

36d3b688

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

jsm28 committed 4 years ago

f94b0b31

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

alreadydone committed 4 years ago

9ceb3c2a

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

eric-wieser committed 4 years ago

436966c1

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

Ruben-VandeVelde committed 4 years ago

7b91f008

Newer Older