leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 3 years ago

d4de29e7

feat(linear_algebra/matrix/determinant): special case of the matrix determinant lemma

eric-wieser committed 3 years ago

7fcf750e

feat(topology/separation): add t2_space_iff (#12628)

kbuzzard committed 3 years ago

d8ef1de0

feat(data/list/infix): add lemmas and instances (#12511)

astrainfinita committed 3 years ago

5242a7fb

refactor(data/set): generalize `set.restrict` and take set argument first in both `set.restrict` and `subtype.restrict` (#12510)

rish987 committed 3 years ago

df3792f8

feat(set_theory/ordinal_topology): Basic results on the order topology of ordinals (#11861)

vihdzp committed 3 years ago

c1edbec8

feat(data/finset/noncomm_prod): finite pi lemmas (#12291)

nomeata committed 3 years ago

09ea7fb0

chore(ci): update trepplein to version 1.1 (#12669)

gebner committed 3 years ago

fc882ff8

feat(set_theory/principal): If `a` isn't additive principal, it's the sum of two smaller ordinals (#12664)

vihdzp committed 3 years ago

abb8e5da

feat(group_theory/commutator): The three subgroups lemma (#12634)

tb65536 committed 3 years ago

cc6e2eb1

chore(topology/homotopy): Move more algebraic-flavored content about fundamental groupoid to algebraic_topology folder (#12631)

prakol16 committed 3 years ago

6a51706d

chore(algebra/category/Module): simp lemmas for monoidal closed (#12608)

kim-em committed 3 years ago

a2544deb

feat(set_theory/{ordinal, ordinal_arithmetic}): Add various instances for `o.out.α` (#12508)

vihdzp committed 3 years ago

31e60c87

feat(data/list/basic): Split and intercalate are inverses (#12466)

prakol16 committed 3 years ago

1f428f3e

feat(category_theory/bicategory/free): define free bicategories (#11998)

yuma-mizuno committed 3 years ago

cd001b2d

feat(analysis/seminorm): add lemmas for inequalities and `finset.sup` (#12650)

mcdoll committed 3 years ago

520f2046

feat(analysis/complex/schwarz): some versions of the Schwarz lemma (#12633)

urkud committed 3 years ago

0f3bfda7

feat(topology/hom/open): Continuous open maps (#12406)

YaelDillies committed 3 years ago

c2368be5

refactor(set_theory/cardinal_ordinal): `aleph_is_principal_aleph` → `principal_add_aleph` (#12663)

vihdzp committed 3 years ago

7b7fea55

feat(set_theory/ordinal): `ord 1 = 1` (#12662)

vihdzp committed 3 years ago

6ebb3786

feat(algebra/support) support of power is subset of support (#12654)

Multramate committed 3 years ago

18ba3950

chore(topology/algebra/group_with_zero): fix docstring for has_continuous_inv0 (#12653)

sgouezel committed 3 years ago

6b3b567f

feat(analysis/seminorm): add lemmas for `with_seminorms` (#12649)

mcdoll committed 3 years ago

1f5950a7

move(topology/sets/*): Move topological types of sets together (#12648)

YaelDillies committed 3 years ago

b6fa3beb

chore(analysis/locally_convex/basic): generalize lemmas and add simple lemmas (#12643)

mcdoll committed 3 years ago

778dfd50

add endofunctor.algebra (#12642)

Jlh18 committed 3 years ago

f8d947c7

refactor(set_theory/ordinal_arithmetic): Turn various results into simp lemmas (#12661)

vihdzp committed 3 years ago

174f1da1

docs(algebra/*): Add docstrings to additive lemmas (#12578)

YaelDillies committed 3 years ago

ad0988b3

feat(analysis/inner_product_space/pi_L2): `linear_isometry.extend` (#12192)

hparshall committed 3 years ago

580e1d95

feat(measure_theory/group/fundamental_domain): ess_sup_measure_restrict (#12603)

AlexKontorovich committed 3 years ago

3751ec63

Older