leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 3 years ago

1dd47ef1

Merge branch 'relabelling_mk'' into more_relabelling_api

vihdzp committed 3 years ago

b9fdba5e

Update short.lean

vihdzp committed 3 years ago

c57da663

vihdzp committed 3 years ago

db6409d1

Merge branch 'relabelling_mk'' into more_relabelling_api

vihdzp committed 3 years ago

3d5ea986

Update pgame.lean

vihdzp committed 3 years ago

69142aed

Merge branch 'relabelling_mk'' into more_relabelling_api

vihdzp committed 3 years ago

1df6f09a

Update pgame.lean

vihdzp committed 3 years ago

44deb8c6

Update pgame.lean

vihdzp committed 3 years ago

b84125f7

Merge branch 'relabelling_mk'' into more_relabelling_api

vihdzp committed 3 years ago

02a1b6a3

vihdzp committed 3 years ago

4bde6952

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

eric-wieser committed 3 years ago

07c83c81

vihdzp committed 3 years ago

c0335261

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

feat(field_theory.intermediate_field): intermediate_field.inclusion (#12596)

Sebastian-Monnet committed 3 years ago

7c2ad75e

feat(data/int/basic): add a better `has_reflect int` instance (#14906)

eric-wieser committed 3 years ago

e420232b

feat(meta/univs): Add a reflect_name tactic, make reflected instances universe polymorphic (#14766)

eric-wieser committed 3 years ago

f05c49f6

feat(data/finset/pointwise): `s • t` is the union of the `a • t` (#14696)

YaelDillies committed 3 years ago

8187142b

feat(ring_theory/trace): Add `trace_eq_sum_automorphisms`, `norm_eq_prod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523)

isadofschi committed 3 years ago

6d00cc21

chore(order/filter): turn `tendsto_id'` into an `iff` lemma (#14791)

urkud committed 3 years ago

efe794c3

feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)

RemyDegenne committed 3 years ago

6cefaf4b

Older