leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 3 years ago

bc091766

Merge branch 'lsub_le' into inaccessible

vihdzp committed 3 years ago

3f9c03c2

Merge branch 'sup_eq_lsub' into inaccessible

vihdzp committed 3 years ago

5ca99bc9

vihdzp committed 3 years ago

20dae173

Proved `sup_eq_lsub_iff_lt_sup`

vihdzp committed 3 years ago

0b1c333f

vihdzp committed 3 years ago

801c9378

vihdzp committed 3 years ago

1fae9fef

feat(topology/algebra/mul_action2): quotient by a properly discontinuous group action is t2 (#10465)

AlexKontorovich committed 3 years ago

6184db11

vihdzp committed 3 years ago

eb7d1abf

vihdzp committed 3 years ago

9cb3bebb

vihdzp committed 3 years ago

1dd7b114

Merge branch 'master' into inaccessible

vihdzp committed 3 years ago

14c905a4

feat(algebra/group/hom): Notation for `monoid_with_zero_hom` (#11632)

YaelDillies committed 3 years ago

4d761f44

feat(combinatorics/simple_graph/coloring): add inequalities from embeddings (#11548)

kmill committed 3 years ago

1b3da831

feat(group_theory/abelianization): add abelianization_of_comm_group (#11467)

nomeata committed 3 years ago

158c0eaf

feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759)

Vierkantor committed 3 years ago

494f7199

feat(model_theory/basic): Terms, formulas, and definable sets (#11067)

awainverse committed 3 years ago

6b322417

feat(README.md): add Kyle Miller as new maintainer (#11653)

kmill committed 3 years ago

4883d11c

feat(number_theory/quadratic_reciprocity): generalise legendre_sym to allow integer first argument (#11573)

alexjbest committed 3 years ago

bf71feb0

feat(group_theory/nilpotent): add nilpotency_class inequalities (#11585)

nomeata committed 3 years ago

f7a597ad

feat(README.md): add Frédéric Dupuis as new maintainer (#11651)

dupuisf committed 3 years ago

f2786639

chore(order/filter, *): enhancing `filter_upwards` tactic (#11624)

arthurpaulino committed 3 years ago

b3cd0e6d

refactor(order/{bounded, rel_classes}): Moved `bounded` into the `set` namespace (#11594)

vihdzp committed 3 years ago

8cc2ff4c

chore(topology/metric_space/gromov_hausdorff): Golf some theorems (#11591)

vihdzp committed 3 years ago

b834415b

feat(algebra/big_operators/basic): add lemma `finset.prod_dvd_prod` (#11521)

stuart-presnell committed 3 years ago

88479be0

refactor(tactic/interactive): rename tactic.interactive.triv to tactic.interactive.trivial' (#11643)

kmill committed 3 years ago

4f5d6acf

feat(README.md): add Riccardo Brasca as new maintainer (#11647)

riccardobrasca committed 3 years ago

0d172bac

feat(data/finset/finsupp): Finitely supported product of finsets (#11639)

YaelDillies committed 3 years ago

12fde093

chore(ci): remove working directory on self-hosted (#11645)

gebner committed 3 years ago

32052b86

feat(algebra/pointwise): add partial order to `set_semiring` (#11567)

adomani committed 3 years ago

511aa358

Older