Commits leanprover-community/mathlib3

feat(linear_algebra/affine_space/affine_subspace): `vector_span_insert_eq_vector_span` (#16765)

jsm28 committed 3 years ago

64b6d04f

refactor(number_theory): reorganize number field results into new subfolder (#16764)

xroblot committed 3 years ago

81120aec

feat(data/{fin,}set/pointwise): add `{fin,}set.inv_insert` (#16748)

urkud committed 3 years ago

8a1b982f

refactor(data/fin/basic): merge `fin.rev` and `order_iso.fin_equiv` (#16745)

urkud committed 3 years ago

c7aa2dfa

fix({ tactic/fin_cases + test/interval_cases }): add `focus1` and a test (#16752)

adomani committed 3 years ago

9dbe038e

feat(category_theory/groupoid/free): free groupoid on a quiver (#16666)

bottine committed 3 years ago

2e433a50

feat(group_theory/subgroup): add several trivial lemmas (#16633)

urkud committed 3 years ago

35bc69bc

feat(data/fintype/basic): Existence of a bijection with specified behaviour on a subset (#16479)

hrmacbeth committed 3 years ago

3cf2547c

chore(analysis/locally_convex/with_seminorms): fix namespaces for dot-notation (#16771)

mcdoll committed 3 years ago

d2461773

feat(analysis/normed/group/add_circle): define the additive circle (#16201)

ocfnash committed 3 years ago

ebe6bda5

feat(algebra/module/projective): weaken assumptions in lifting_property (#16750)

antoinelab01 committed 3 years ago

08bb56fb

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

leanprover-community-bot committed 3 years ago

8818d823

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