leanprover-community/mathlib3

Pull Requests Commits

chore(topology/algebra/module/basic): remove `continuous_linear_map.ker` and `continuous_linear_map.range` (#16208)

dupuisf committed 3 years ago

3397560e

chore(number_theory/legendre_symbol/norm_num): remove now unnecessary instance (#16659)

MichaelStollBayreuth committed 3 years ago

e2621d93

Merge branch 'fin-inf-group-type-tags' into fg-surj

mlavrent committed 3 years ago

ca316868

Add finite & infinite instances to additive and multiplicative

mlavrent committed 3 years ago

c5c3b371

Move instances of finite and infinite to type_tags

mlavrent committed 3 years ago

c48d8639

feat(analysis/normed_space/operator_norm): remove to_span_singleton_norm (#16654)

fpvandoorn committed 3 years ago

e46daa0a

chore(analysis/special_functions/pow): squeezing some simps (#16660)

mcdoll committed 3 years ago

1a4f9279

feat(algebra/category/Group/injective): divisible groups are injective in category of `AddCommGroup` (#16110)

jjaassoonn committed 3 years ago

ab2e9fb6

chore(analysis/special_functions/pow): squeeze a nonterminal simp (#16657)

mcdoll committed 3 years ago

b3d23d74

feat(topology/uniform_space/completion): add uniform_completion.complete_equiv_self (#16612)

xroblot committed 3 years ago

9f972c7e

feat(topology/sheaves/skyscraper): define skyscraper presheaves and calculate stalks (#15934)

jjaassoonn committed 3 years ago

f38b4dfe

chore(number_theory/padics): stylistic changes (#15755)

Multramate committed 3 years ago

db24ba7c

perf(analysis/normed_space/continuous_affine_map): Speedup (#16652)

YaelDillies committed 3 years ago

a12363e2

doc(analysis/special_functions/stirling): fix equation (#16651)

fpvandoorn committed 3 years ago

b41babaa

feat(data/fintype/basic): `set.to_finset_of_finset` (#16460)

kmill committed 3 years ago

dfd17f2f

feat(real/ennreal): basic lemmas about `ennreal.to_nnreal` and `ennreal.to_real` (#16318)

dtumad committed 3 years ago

a44ce4da

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

mlavrent committed 3 years ago

9db7777a

Newer Older