leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into game_cmp

vihdzp committed 3 years ago

47aa17d5

Update pgame.lean

vihdzp committed 3 years ago

daff18b6

vihdzp committed 3 years ago

9ae4c8ec

feat: `add_monoid_with_one`, `add_group_with_one` (#12182)

gebner committed 3 years ago

32b08ef8

feat(data/zmod/algebra): add subsingleton instance for zmod-algebras (#14946)

ericrbg committed 3 years ago

871fcd87

feat(set_theory/ordinal/notation): fast growing hierarchy (#14072)

digama0 committed 3 years ago

e0ecaa9e

Update nim.lean

vihdzp committed 3 years ago

a2033107

vihdzp committed 3 years ago

079e5233

boilerplate hell

vihdzp committed 3 years ago

afeabe42

vihdzp committed 3 years ago

28ee7d0e

feat(data/{finset,set}/basic): More `∪`/`∩` laws (#14952)

YaelDillies committed 3 years ago

cfbb97f7

feat(data/set/lattice): Preimages are disjoint iff the sets are disjoint (#14951)

YaelDillies committed 3 years ago

ccb1cf38

basic API on pre-game comparison

vihdzp committed 3 years ago

5720e911

feat(order/symm_diff): The symmetric difference is involutive (#14959)

YaelDillies committed 3 years ago

72cff840

refactor(*): Use `finset.Iix`/`finset.Ixi` (#14448)

YaelDillies committed 3 years ago

b8c3e61b

feat(data/fintype/basic): Constructing an equivalence from a left inverse (#14816)

YaelDillies committed 3 years ago

7ee73e4a

feat(algebra/field/basic): Semifields (#14683)

YaelDillies committed 3 years ago

88127521

feat(analysis/normed*): add instances about balls and spheres (#14808)

urkud committed 3 years ago

f9571f0f

chore(*): golf (#14939)

urkud committed 3 years ago

6f923bd9

feat(linear_algebra/clifford_algebra/of_alternating): extend alternating maps to the exterior algebra (#14803)

eric-wieser committed 3 years ago

07c83c81

feat(representation_theory/character): characters of representations (#14453)

antoinelab01 committed 3 years ago

4fd263ba

feat(algebra/indicator_function): add an apply version of `mul_indicator_finset_bUnion` (#14919)

kex-y committed 3 years ago

8bf85d74

feat(probability/martingale): add some lemmas for submartingales (#14904)

kex-y committed 3 years ago

f94a64f7

feat(topology/metric_space): a countably generated uniformity is metrizable (#14052)

urkud committed 3 years ago

40fa2d84

refactor(algebra/order/monoid): use typeclasses instead of lemmas (#14848)

urkud committed 3 years ago

fe322e12

feat(linear_algebra/{multilinear, alternating}): add `cod_restrict` and lemmas (#14927)

eric-wieser committed 3 years ago

0e5f278d

feat(data/finite/basic): add missing instances (#14913)

urkud committed 3 years ago

3e326fcb

chore(topology/basic): golf a proof (#14911)

urkud committed 3 years ago

363bbd22

refactor(data/polynomial): extract/add lemmas and golf (#14888)

alreadydone committed 3 years ago

475cf379

feat(probability/independence): equivalent ways to check indep_fun (#14814)

RemyDegenne committed 3 years ago

dabb0c61

Older