Commits leanprover-community/mathlib3

erdOne committed 3 years ago

055a2a4f

Merge branch 'master' of https://github.com/leanprover-community/mathlib into dimension_theory

erdOne committed 3 years ago

bd80ae38

feat(analysis/convex/cone/basic): add `has_add`, `add_zero_class`, and `add_comm_semigroup` instances to `convex_cone` (#16213)

apurvnakade committed 3 years ago

3665254a

feat(linear_algebra/matrix/hermitian): complex_hermitian_real_diagonal (#16380)

mapehe committed 3 years ago

a4e0a656

feat(order/liminf_limsup): add limsup/liminf variants of some Limsup/Liminf lemmas (#16759)

RemyDegenne committed 3 years ago

b2d70ba0

docs(analysis/locally_convex/bounded): fix hyperlink (#16753)

mcdoll committed 3 years ago

2ce380c2

chore(data/analysis/*): Fix lint and docs (#16751)

YaelDillies committed 3 years ago

51696a64

chore(analysis/locally_convex/[continuous_of_]bounded): import `analysis.normed_space.is_R_or_C` later (#16758)

ADedecker committed 3 years ago

2bb1bae8

feat(data/fintype): complement of univ (#16623)

b-mehta committed 3 years ago

c4878d17

feat(analysis/locally_convex/with_seminorms): boundedness of images (#16674)

mcdoll committed 3 years ago

b2381e5a

feat(analysis/locally_convex): first countable topologies from countable families of seminorms (#16595)

mcdoll committed 3 years ago

73d05c46

feat(analysis/convex/body): define bodies and implement module instance (#16297)

datokrat committed 3 years ago

df6a0b2e

feat(algebraic_topology): extra degeneracy of augmented simplicial objects (#16411)

joelriou committed 3 years ago

d79c3671

feat(topology/sheaves/skyscraper): skyscraper presheaf as a functor (#16685)

jjaassoonn committed 3 years ago

f063221a

chore(topology,analysis): make the sup metric and norm computable (#16570)

eric-wieser committed 3 years ago

852b23b5

feat(analysis/locally_convex/with_seminorms): split `continuous_from_bounded` to get an extra continuity criterion (#16710)

ADedecker committed 3 years ago

77db6f75

feat(group_theory/subgroup/basic): If `H` is commutative, then `H ≤ H.centralizer` (#16718)

tb65536 committed 3 years ago

d638c7f7

refactor(analysis/inner_product_space/pi_L2): Delete `orthonormal_basis_index` (#16698)

YaelDillies committed 3 years ago

567220c2

feat(order/filter/*,topology/noetherian_space): add lemmas about `cofinite` (#16498)

urkud committed 3 years ago

ba197e48

feat(topology/algebra/module/character_space): kernels of terms of the `character_space` (#16722)

j-loreaux committed 3 years ago

7f034c52

feat(data/list/basic): `λ a, [a]` is injective (#16716)

urkud committed 3 years ago

c2d85cec

feat(analysis/convolution): prove that parametric convolution tends to a specific value (#16704)

fpvandoorn committed 3 years ago

21347ef2

feat(analysis/locally_convex): locally bounded implies continuous (#16550)

mcdoll committed 3 years ago

180f4f20

feat(number_theory/number_field): add mem_roots_of_unity_of_norm_eq_one (#15143)

xroblot committed 3 years ago

bf783181

feat(topology/sheaves/skyscraper): skyscraper presheaf is a sheaf (#16649)

jjaassoonn committed 3 years ago

7295c811

feat(category_theory/morphism_property): miscellaneous basic results (#16444)

joelriou committed 3 years ago

8150c5eb

feat(algebraic_topology/dold_kan): decomposition of Q (#16357)

joelriou committed 3 years ago

9af20344

feat(algebraic_topology/simplex_category): strong epi mono factorisations (#16276)

joelriou committed 3 years ago

563aed34

feat(*): generalize to and add distrib_smul instances (#16132)

Vierkantor committed 3 years ago

8f78eb9c

chore(number_theory/bernoulli_polynomials): removed unnecessary cast_succ from sum_bernoulli (#16731)

jreaso committed 3 years ago

25c8333e