leanprover-community/mathlib

Pull Requests Commits

j-loreaux committed 3 years ago

Verified da5da889

move and clean up

j-loreaux committed 3 years ago

Verified 0213881b

forget_to_Algebra

j-loreaux committed 3 years ago

Verified dfae6f00

add a bunch of basics

j-loreaux committed 3 years ago

Verified 54140a6f

define the category of unital C⋆-algebras.

j-loreaux committed 3 years ago

Verified ff0463f0

simplify with better `variables` declarations

j-loreaux committed 3 years ago

Verified ce125583

define `star_alg_equiv`s and provide basic API

j-loreaux committed 3 years ago

Verified 22db639b

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

Older