leanprover-community/mathlib

Pull Requests Commits

BoltonBailey committed 3 years ago

a0b63b09

add repetition code as inhabited instance

BoltonBailey committed 3 years ago

13bb42d8

BoltonBailey committed 3 years ago

5ee9e76b

BoltonBailey committed 3 years ago

f520e643

BoltonBailey committed 3 years ago

f988de66

BoltonBailey committed 3 years ago

6b70943f

feat(topology/sheaves/abelian): category of sheaves is abelian (#16403)

jjaassoonn committed 3 years ago

d5e1961f

feat(group_theory/subgroup/basic): golf proof of instance normal_inf_normal (#16620)

faenuccio committed 3 years ago

525ffd73

feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set. (#15259)

jjaassoonn committed 3 years ago

ebf8ff42

feat(data/option/basic): `option.map` is injective (#16626)

urkud committed 3 years ago

3b4e9d58

feat(data/list/basic): `list.head`, `list.head'`, and `list.tail` are surjective (#16625)

urkud committed 3 years ago

a48b8eff

feat(combinatorics/simple_graph/density): `positivity` extension for `edge_density` (#16640)

YaelDillies committed 3 years ago

19deedcc

chore(number_theory/cyclotomic): fix typo in lemma name (#16643)

alexjbest committed 3 years ago

653307ac

feat(linear_algebra/ray): `iff` versions of some lemmas (#16642)

jsm28 committed 3 years ago

765955fb

chore(data/list/range): fix incorrect docstring (#16622)

b-mehta committed 3 years ago

a337782b

feat(data/real/ennreal): make of_real_sub easier to rewrite with (#16621)

b-mehta committed 3 years ago

74f6e95c

chore(.docker): fix build failure in docker images (#16590)

kim-em committed 3 years ago

868ee2c6

refactor(linear_algebra/affine_space): remove `open_locale classical` (#16628)

jsm28 committed 3 years ago

5a8eded1

feat(algebra/order/hom/monoid): add `monotone_iff_map_nonneg/pos` + golf (#16601)

alreadydone committed 3 years ago

4a927b25

feat(analysis/inner_product_space/l2_space): compute orthogonal projection on U given a hilbert basis of U (#15541)

ADedecker committed 3 years ago

1313934b

feat(algebra/module/basic): More general `smul_ne_zero` (#16608)

YaelDillies committed 3 years ago

3b727dc2

chore(category_theory/preadditive/biproducts): speed up biprod.of_components_eq (#16516)

Ruben-VandeVelde committed 3 years ago

8f09a402

feat(order/symm_diff): Heyting bi-implication (#16544)

YaelDillies committed 3 years ago

8cd94b84

chore(tactic/{core + compute_degree}): tightening up compute_degree_le (#15649)

adomani committed 3 years ago

2d915e4e

feat(data/complex/basic): bundle complex.abs (#16347)

ericrbg committed 3 years ago

ba80091d

chore(scripts): update nolints.txt (#16618)

leanprover-community-bot committed 3 years ago

5947fb69

chore(linear_algebra/matrix/adjugate): remove unnecessary fin_cases with (#16605)

kim-em committed 3 years ago

44eb23a5

chore(data/finset/basic): Scope variables over smaller sections (#16613)

eric-wieser committed 3 years ago

ac01c538

feat(algebra/punit_instances): linear_ordered_add_comm_monoid_with_top punit (#16609)

ericrbg committed 3 years ago

27b90386

chore(docs): run `bibtool` on `references.bib` (#16606)

eric-wieser committed 3 years ago

01894cc4

Older