leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into jjaassoonn/sheaf_abelian

jjaassoonn committed 3 years ago

420725a7

Apply suggestions from code review

jjaassoonn committed 3 years ago

Verified 282c3915

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

feat(topology/separation): connected sets in a t1 space are infinite (#16584)

ericrbg committed 3 years ago

8deb2a68

doc(group_theory/sylow): update docstring to include card_eq_multiplicity as a main result (#14354)

ChrisHughes24 committed 3 years ago

e1783b0f

feat(group_theory/group_action): define `distrib_smul` and `smul_zero_class` (#16123)

Vierkantor committed 3 years ago

8f66240c

feat(category_theory/limits/shapes/biproducts): more (co)kernel instances (#14188)

kim-em committed 3 years ago

249a9c91

feat(order/filter/lift): replace some implications with iffs (#16452)

urkud committed 3 years ago

313f36d4

chore(data/finset/basic): move `disjoint` proofs earlier (#16436)

eric-wieser committed 3 years ago

24b50bfc

feat(analysis/normed_space/affine_isometry): `subtypeₐᵢ` (#16573)

jsm28 committed 3 years ago

d0507e7b

chore(tactic): typos in docs (#16510)

kim-em committed 3 years ago

f89fa08b

feat(topology/subset_properties): an infinite type with cofinite topology is irreducible (#16499)

urkud committed 3 years ago

02022cd6

Older