leanprover-community/mathlib

Pull Requests Commits

slight optimization

alreadydone committed 4 years ago

123055f9

proof of compatibility for transferred lax functor

alreadydone committed 4 years ago

52cb146d

pseudofunctor transfer by adjunction

alreadydone committed 4 years ago

c920a07a

adjunction/mates: new lemmas/easy defs

alreadydone committed 4 years ago

d2bac998

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

refactor(linear_algebra/eigenspace): refactor `eigenvectors_linearly_independent` (#10198)

hrmacbeth committed 4 years ago

75207e91

feat(measure_theory/probability_mass_function): Define a measure assosiated to a pmf (#9966)

dtumad committed 4 years ago

1019dd67

feat(category_theory/sites/*): Dense subsite (#9694)

erdOne committed 4 years ago

9e1e4f01

chore(measure_theory): move `mutually_singular` to a new file (#10281)

urkud committed 4 years ago

6fd688b5

feat(category_theory/limits): Cone limiting iff terminal. (#10266)

erdOne committed 4 years ago

d7e320e6

feat(analysis/normed_space/star): introduce C*-algebras (#10145)

dupuisf committed 4 years ago

e5a79a7a

feat(field_theory/splitting_field): add eval_root_derivative_of_split (#10224)

riccardobrasca committed 4 years ago

d6056eee

feat(category_theory/limits/concrete_category): A lemma about concrete multiequalizers (#10277)

adamtopaz committed 4 years ago

73b2b651

feat(field_theory/separable): X^n - 1 is separable iff ↑n ≠ 0. (#9779)

ericrbg committed 4 years ago

0b4c5409

chore(category_theory/isomorphisms): Adjust priority for is_iso.comp_is_iso (#10276)

adamtopaz committed 4 years ago

8cd5f0ee

feat(linear_algebra/pi_tensor_product): add subsingleton_equiv (#10274)

eric-wieser committed 4 years ago

d6860258

feat(measure_theory): integral over a family of pairwise a.e. disjoint sets (#10268)

urkud committed 4 years ago

f99d6386

Older