Commits leanprover-community/mathlib

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

perf(algebraic_topology/simplicial_object): Speedup `simplicial_cosimplicial_augmented_equiv` (#16729)

YaelDillies committed 3 years ago

2a543b0d

feat(group_theory/schreier): The size of the commutator subgroup is bounded in terms of the index of the center and the number of commutators (#16679)

tb65536 committed 3 years ago

5fefdfa1

refactor(ring_theory/polynomial/tower): review APIs (#16678)

astrainfinita committed 3 years ago

7aebb349

feat(linear_algebra/{basis, determinant, orientation}): determinant of `adjust_to_orientation` of a basis (#16476)

hrmacbeth committed 3 years ago

a753abcf

feat(topology/semicontinuous): characterization by closed sets of semicontinuous maps to a linear order (#16442)

ADedecker committed 3 years ago

c1a28cb2

feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373)

TwoFX committed 3 years ago

e4ee4e30