Commits leanprover-community/mathlib3

Eliminating `finish`es and non-terminal `simp`s

stuart-presnell committed 4 years ago

13b0ca8f

feat(number_theory/divisors): prime divisors

stuart-presnell committed 4 years ago

8349c2af

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

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