leanprover-community/mathlib3

Pull Requests Commits

BoltonBailey committed 3 years ago

109a5b6c

BoltonBailey committed 3 years ago

c0687251

Merge master to fix CI

kim-em committed 3 years ago

883da65b

feat(linear_algebra/dual): dual of a finite free module is finite free (#13896)

antoinelab01 committed 3 years ago

9503f733

refactor(set_theory/game/ordinal): Improve API (#13878)

vihdzp committed 3 years ago

eb1a566f

feat(set_theory/game/nim): Add basic API (#13857)

vihdzp committed 3 years ago

28568bdb

feat(logic/equiv/set): equivalences between all preimages gives an equivalence of domains (#13853)

kim-em committed 3 years ago

a80e5683

feat(set_theory/game/nim): `nim 0` is a relabelling of `0` and `nim 1` is a relabelling of `star` (#13846)

vihdzp committed 3 years ago

edf6cefa

feat(algebra/ring/idempotents): Introduce idempotents (#13830)

mans0954 committed 3 years ago

fd8474f5

feat(analysis/normed_space/weak_dual): add the rest of Banach-Alaoglu theorem (#9862)

kkytola committed 3 years ago

91c0ef86

BoltonBailey committed 3 years ago

8c675748

ci(workflows/dependent-issues): run once every 15 mins, instead of on every merged PR (#13940)

jcommelin committed 3 years ago

90d6f271

chore(analysis/analytic_composition): weaken some typeclass arguments (#13924)

eric-wieser committed 3 years ago

aabcd895

feat(set_theory/game/{pgame, basic}): Add more order lemmas (#13807)

vihdzp committed 3 years ago

209bb5d4

feat(representation/Rep): linear structures (#13782)

kim-em committed 3 years ago

31529827

refactor(linear_algebra/charpoly): split file to reduce imports (#13778)

kim-em committed 3 years ago

0009ffba

refactor(algebra/restrict_scalars): remove global instance on module_orig (#13759)

kim-em committed 3 years ago

dd4590af

fix(src/tactic/alias): Teach `get_alias_target` about `alias f ↔ a b` (#13742)

nomeata committed 3 years ago

abcd601c

feat(data/int/cast): int cast division lemmas (#13929)

b-mehta committed 3 years ago

0038a043

feat(set_theory/game/birthday): More basic lemmas on birthdays (#13729)

vihdzp committed 3 years ago

46023701

feat(group_theory/complement): API lemmas relating `range_mem_transversals` and `to_equiv` (#13694)

tb65536 committed 3 years ago

60ad8448

feat(group_theory/free_group): is_free_group via `free_group X ≃* G` (#13633)

nomeata committed 3 years ago

923ae0bc

feat(number_theory/cyclotomic/rat): the ring of integers of cyclotomic fields. (#13585)

riccardobrasca committed 3 years ago

552a4709

feat(algebra/homology/Module): API for complexes of modules (#12622)

kim-em committed 3 years ago

e7161393

feat(set_theory/cardinal/cofinality): Cofinality of normal functions (#12384)

vihdzp committed 3 years ago

a7c50973

feat(analysis/convex/topology): Separating by convex sets (#11458)

YaelDillies committed 3 years ago

d565adb7

feat(measure_theory/integral/lebesgue): speed up a proof (#13946)

sgouezel committed 3 years ago

32320a10

fix(ring_theory/polynomial/basic): fix unexpected change of an implicit parameter (#13935)

astrainfinita committed 3 years ago

ceca8d74

feat(linear_algebra/span): add `finite_span_is_compact_element` (#13901)

haruhisa-enomoto committed 3 years ago

53c79d56

feat(order/basic): Notation for `order_dual` (#13798)

YaelDillies committed 3 years ago

a057441e

Older