leanprover-community/mathlib

Pull Requests Commits

feat(algebraic_geometry/open_immersion): Operations on open covers. (#11442)

erdOne committed 4 years ago

5a6c13bc

feat(algebra/ne_zero): `pos_of_ne_zero_coe` (#11437)

ericrbg committed 4 years ago

e2860129

feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class (#11434)

eric-wieser committed 4 years ago

021baaee

feat(topology): some improvements (#11424)

fpvandoorn committed 4 years ago

61054f70

feat(combinatorics/configuration): Define the order of a projective plane (#11430)

tb65536 committed 4 years ago

3c1740ac

feat(topology/subset_properties): some compactness properties (#11425)

fpvandoorn committed 4 years ago

5a3abca1

feat(algebraic_geometry): lemmas about basic opens in schemes (#11393)

erdOne committed 4 years ago

feaf6f5e

feat(data/{multiset,finset}/sum): Disjoint sum of multisets/finsets (#11355)

YaelDillies committed 4 years ago

85accb8a

feat(analysis/inner_product_space/l2): Inner product space structure on `l2` (#11315)

hrmacbeth committed 4 years ago

9a949936

fix(algebra/star/basic): redefine `star_ordered_ring` (#11213)

dupuisf committed 4 years ago

fb2b1a01

feat(tactic/lint): include linter name in github output (#11413)

robertylewis committed 4 years ago

60c77d49

feat(algebraic_geometry): Gluing schemes (#11431)

erdOne committed 4 years ago

d2484474

chore(data/list/big_operators): rename vars, reorder lemmas (#11433)

urkud committed 4 years ago

48fd9f25

feat(set_theory/ordinal_arithmetic): Families of ordinals (#11278)

vihdzp committed 4 years ago

e830348b

feat(algebra/lie/nilpotent): central extensions of nilpotent Lie modules / algebras are nilpotent (#11422)

ocfnash committed 4 years ago

6fa2e46e

feat(analysis/normed_space/linear_isometry): add congr_arg and congr_fun (#11428)

eric-wieser committed 4 years ago

432e85ef

feat(analysis/mean_inequalities): Hölder's inequality for infinite sums (#11314)

hrmacbeth committed 4 years ago

8a13846e

feat(analysis/inner_product_space/basic): criterion for summability (#11224)

hrmacbeth committed 4 years ago

05044255

feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly (#11420)

riccardobrasca committed 4 years ago

6446ba8f

fix(analysis/calculus/fderiv_symmetric): speed up tactic block from 3.6s to 180ms (#11426)

eric-wieser committed 4 years ago

ea9f964b

feat(measure_theory/function/uniform_integrable): Egorov's theorem (#11328)

kex-y committed 4 years ago

0f79668f

chore(order/lattice_intervals): review (#11416)

urkud committed 4 years ago

a16a5b5b

feat(linear_algebra/{cross_product,vectors}): cross product (#11181)

madvorak committed 4 years ago

cd4f5c40

feat(data/nat/periodic): periodic functions for nat (#10888)

BoltonBailey committed 4 years ago

799cdbb2

feat(algebraic_geometry): Gluing presheafed spaces (#10269)

erdOne committed 4 years ago

6609204b

chore(ring_theory/roots_of_unity): change argument order (#11415)

ericrbg committed 4 years ago

e6db2457

feat(order,data/set/intervals): lemmas about `is_bot`/`is_top` (#11412)

urkud committed 4 years ago

0c844566

doc(number_theory/cyclotomic/basic): fix docstrings (#11411)

ericrbg committed 4 years ago

3f1ac6c5

feat(combinatorics/configuration): Cardinality results for projective plane. (#11406)

tb65536 committed 4 years ago

e839c9ae

refactor(linear_algebra/affine_space): move def of `slope` to a new file (#11361)

urkud committed 4 years ago

12b6b993

Newer Older