leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' of github.com:leanprover-community/mathlib into fg-surj

mlavrent committed 3 years ago

4a7d9dba

feat(data/set/basic): Refactor and additions of sep lemmas (#16566)

linesthatinterlace committed 3 years ago

35f0f1ba

feat(algebra/order/floor): Positivity extensions for `floor` and `ceil` (#16635)

YaelDillies committed 3 years ago

4dc217e4

refactor(algebra/group/defs): `inv_one_class`, `neg_zero_class` (#16187)

jsm28 committed 3 years ago

7247a3cc

Merge branch 'master' into fg-surj

mlavrent committed 3 years ago

8ddff7ca

feat(topology/order/lattice): add `topological_lattice` instance for linear orders with an order closed topology (#16664)

j-loreaux committed 3 years ago

60851c93

feat(analysis/schwartz_space): add lemmas for seminorms (#16634)

mcdoll committed 3 years ago

8ef6d8f2

feat(linear_algebra/affine_space/affine_subspace): `parallel` (#16298)

jsm28 committed 3 years ago

494b1f8e

feat(algebra/jordan/special): The symmetrization of an associative ring is a commutative Jordan multiplication (#11401)

mans0954 committed 3 years ago

6fe90f28

feat(order/atoms): link `set` to `is_atom` API (#16665)

j-loreaux committed 3 years ago

c251522d

feat(group_theory/finiteness): Add variants of `rank_closure_le_card` (#16364)

tb65536 committed 3 years ago

999e0925

feat(analysis/normed_space/star/basic): in a C⋆-ring `star x * x = 0 ↔ x = 0` (#16672)

j-loreaux committed 3 years ago

8e8c7fd5

chore(ring_theory/(mv_)polynomial/{symmetric, homogeneous}): move files (#16414)

astrainfinita committed 3 years ago

99e885b9

feat(topology/algebra/[uniform_]group): more `ext` lemmas (#16667)

ADedecker committed 3 years ago

ec74a7cc

feat(algebra/group/type_tags): finite & infinite instances for additive/multiplicative group type tags (#16662)

mlavrent committed 3 years ago

a652850a

fix(tactic/positivity + test): instantiate meta-variables and add a test (#16647)

adomani committed 3 years ago

6f9edf5b

feat(analysis/locally_convex): boundedness in normed spaces (#16636)

mcdoll committed 3 years ago

3bfcb4ce

feat(analysis/calculus): add lemma for norm of zeroth iterated derivative (#16631)

mcdoll committed 3 years ago

c433ac05

feat(data/list/chain): add `list.chain'_is_infix` (#16627)

urkud committed 3 years ago

d0f92493

chore(probability/martingale): use volume_tac in definitions (#16619)

RemyDegenne committed 3 years ago

7a4b066c

feat(geometry/euclidean/basic): angles in subspaces (#16610)

jsm28 committed 3 years ago

89417b90

chore(topology/separation): rename `separated` to `separated_nhds` (#16604)

urkud committed 3 years ago

33c6eeae

feat(topology/subset_properties): lemmas about `disjoint`, `nhds_set`, and `is_compact` (#16591)

urkud committed 3 years ago

dc1ac244

refactor(tactic/lift): remove attribute/simp-set and swap side goal (#16565)

jcommelin committed 3 years ago

801c013f

mlavrent committed 3 years ago

81dc6e6b

mlavrent committed 3 years ago

7bc86e2d

feat(analysis/convex/topology): connectedness and `same_ray` (#16661)

jsm28 committed 3 years ago

f48c65aa

feat(topology/instances/real): classify discrete subgroups (#16592)

hrmacbeth committed 3 years ago

72944168

feat(group_theory/exponent): `card G ∣ exponent G ^ rank G` (#16354)

tb65536 committed 3 years ago

ac49df81

feat(combinatorics/quiver/path): Turn a quiver path into a list (#15240)

YaelDillies committed 3 years ago

3c139aa9

Older