leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 3 years ago

1495200e

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

basic API on pre-game comparison

vihdzp committed 3 years ago

5720e911

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

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

feat(data/real/{e,}nnreal): add some order isomorphisms (#14900)

urkud committed 3 years ago

ac2e9dbf

Older