Commits leanprover-community/mathlib

feat(data/fin/tuple): add `dtuple` and `tuple` type aliases

eric-wieser committed 4 years ago

72543dd0

feat(linear_algebra/alternating): add alternating_map.comp_linear_map (#10314)

eric-wieser committed 4 years ago

1b51fe0f

feat(measure_theory): drop some unneeded assumptions (#10319)

urkud committed 4 years ago

8728e85b

feat(data/equiv/module): add module.to_module_End (#10300)

eric-wieser committed 4 years ago

5307dc1b

chore(data/fin/basic): move tuple stuff to a new file (#10295)

eric-wieser committed 4 years ago

299af47c

feat(data/nat/basic): Some `nat.find` lemmas (#10263)

YaelDillies committed 4 years ago

7dc33bf7

feat(data/list/big_operators): When `list.sum` is strictly positive (#10282)

YaelDillies committed 4 years ago

dd72ebc0

feat(algebra/lie/basic): add missing `@[ext]` and `@[simp]` lemmas (#10316)

urkud committed 4 years ago

bca82787

refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313)

urkud committed 4 years ago

3b5edd06

feat(ring_theory,algebraic_geometry): Miscellaneous lemmas/def/typo corrections (#10307)

alreadydone committed 4 years ago

d8c87253

feat(measure_theory/group): define a few `measurable_equiv`s (#10299)

urkud committed 4 years ago

ca56c5ad

feat(*/{group,mul}_action): more lemmas (#10308)

urkud committed 4 years ago

3578403f

chore(data/equiv/*): rename `trans_symm` and `symm_trans` to `self_trans_symm` and `symm_trans_self`. (#10309)

eric-wieser committed 4 years ago

b91d3449

chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298)

dtumad committed 4 years ago

869cb328

feat(linear_algebra/bilinear_form): add is_refl and ortho_sym for alt_bilin_form (#10304)

mcdoll committed 4 years ago

a7e38a03

feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an `orthogonal_family` (#10208)

hrmacbeth committed 4 years ago

a2323660

feat(category_theory/sites/plus): If P is a sheaf, then the map from P to P^+ is an isomorphism. (#10297)

adamtopaz committed 4 years ago

8bb0b6f7

feat(data/nat/basic): recursion for set nat (#10273)

stuart-presnell committed 4 years ago

55534c4f

feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension) (#9995)

hrmacbeth committed 4 years ago

6afda884

feat(category_theory/sites/sheaf): Add sheaf conditions in terms of multiforks/multiequalizers. (#10294)

adamtopaz committed 4 years ago

f0a98494

chore(analysis/special_functions/trigonometric/complex): put results about derivatives into a new file (#10156)

RemyDegenne committed 4 years ago

adb5c2d6

feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201)

ocfnash committed 4 years ago

62621659

fix(algebra/graded_monoid): correct nonexistent names in tactic defaults (#10293)

eric-wieser committed 4 years ago

b9f7b4db

chore(linear_algebra/multilinear): add const_of_is_empty (#10291)

eric-wieser committed 4 years ago

d7b5ffa0

doc(field_theory/separable): typo (#10290)

ericrbg committed 4 years ago

c5027c91

feat(group_theory/complement): `is_complement'.sup_eq_top` (#10230)

tb65536 committed 4 years ago

6cd63207

doc(README): add list of emeritus maintainers (#10288)

jcommelin committed 4 years ago

07be9042

feat(category_theory/sites/plus): `P⁺` for a presheaf `P`. (#10284)

adamtopaz committed 4 years ago

b51335c4

feat(measure_theory): define `measurable_space` instance on a quotient (#10275)

urkud committed 4 years ago

e6790930

chore(analysis/special_functions/pow): put lemmas about derivatives into a new file (#10153)

RemyDegenne committed 4 years ago

c45e70ac