leanprover-community/mathlib

Pull Requests Commits

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

refactor(order/complete_lattice): `Sup` lemmas before `Inf` lemmas (#14868)

vihdzp committed 3 years ago

cb948930

chore(*): Disparate generalizations to division monoids (#14686)

YaelDillies committed 3 years ago

649ca66b

feat(data/finset): add some lemmas about `finset.disj_union` (#14910)

eric-wieser committed 3 years ago

56185bdd

refactor(ring_theory): generalize basic API of `ring_hom` to `ring_hom_class` (#14756)

dupuisf committed 3 years ago

198cb64d

chore(data/nat,int): move field-specific lemmas about cast (#14890)

Vierkantor committed 3 years ago

44d3fc00

feat(data/set): replace `set_coe.can_lift` by `subtype.can_lift` (#14792)

urkud committed 3 years ago

c3e3d1aa

feat(analysis/../log): log_nat_eq_sum_factorization (#14782)

ericrbg committed 3 years ago

4de20c56

Newer Older