leanprover-community/mathlib

Pull Requests Commits

feat(data/sym/sym2): mem_map/mem_congr/map_id' (#13437)

kmill committed 4 years ago

0c2d68a0

feat(analysis/normed_space/pointwise): Balls disjointness (#13379)

YaelDillies committed 4 years ago

d6c1cf16

chore(ring_theory/ideal/local_ring): generalize to semirings (#13341)

yuma-mizuno committed 4 years ago

2194eef2

feat(number_theory/padics/padic_numbers): add padic.add_valuation (#12939)

mariainesdff committed 4 years ago

c65bebb5

chore(*): clean up unnecessary uses of nat.cases_on (#13454)

alexjbest committed 4 years ago

bbbea1c1

feat(analysis/normed_space/basic): `pi` and `prod` are `normed_algebra`s (#13442)

eric-wieser committed 4 years ago

ebc8b441

feat(group_theory/group_action/conj_act): conjugation by the units of a monoid (#13439)

eric-wieser committed 4 years ago

d13f291b

feat(combinatorics/simple_graph/subgraph): delete_edges (#13306)

kmill committed 4 years ago

dd51529f

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

leanprover-community-bot committed 4 years ago

d6a46b79

chore(analysis/normed_space/multilinear): use notation (#13452)

urkud committed 4 years ago

6a5764b3

feat(topology/algebra/module/multilinear): relax requirements for `continuous_multilinear_map.mk_pi_algebra` (#13426)

eric-wieser committed 4 years ago

d81cedb1

chore(number_theory/zsqrtd/*): Missing docstrings and cleanups (#13445)

YaelDillies committed 4 years ago

1506335d

feat(combinatorics/simple_graph/connectivity): define connected components (#12766)

kmill committed 4 years ago

cbf3062b

feat(group_theory/subgroup/basic): One more `mem_normalizer_iff` lemma (#13395)

tb65536 committed 4 years ago

251bd842

feat(combinatorics/additive/salem_spencer): Salem-Spencer sets under images (#13279)

YaelDillies committed 4 years ago

8bbc5ac4

feat(measure_theory/card_measurable_space): `generate_measurable_rec s` gives precisely the generated sigma-algebra (#12462)

vihdzp committed 4 years ago

fecdd4b2

feat(topology/algebra/order/compact): Sup is continuous (#13347)

fpvandoorn committed 4 years ago

adfe9c7f

feat(analysis/normed_space/finite_dimension): a finite dimensional affine subspace is closed (#13440)

urkud committed 4 years ago

936eb7ee

feat(ring_theory/multiplicity): int.nat_abs (#13420)

BoltonBailey committed 4 years ago

9631a913

feat(measure_theory/constructions/pi): more `measure_preserving` lemmas (#13404)

urkud committed 4 years ago

88ba31c9

refactor(group_theory/schur_zassenhaus): Golf using `is_complement'_stabilizer` (#13392)

tb65536 committed 4 years ago

dd34ffaf

feat(group_theory/complement): Add more API for the action on left transversals (#13363)

tb65536 committed 4 years ago

15b764d8

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13362)

tb65536 committed 4 years ago

769ec8c8

chore(order/complete_lattice): General cleanup (#13323)

vihdzp committed 4 years ago

3676f11d

feat(category_theory): turn a split mono with cokernel into a biproduct (#13184)

javra committed 4 years ago

7bb10813

feat(number_theory/legendre_symbol): add directory legendre_symbol and move quadratic_reciprocity.lean into it (#13441)

MichaelStollBayreuth committed 4 years ago

2693ab58

feat(topology/unit_interval): add lemmas (#13344)

fpvandoorn committed 4 years ago

eb2780b6

chore(data/nat/factorial): tidy (#13436)

ericrbg committed 4 years ago

87f8076f

feat(data/mv_polynomial): add support_X_pow (#13435)

alexjbest committed 4 years ago

dac4f18f

feat(complex/roots_of_unity): extensionality (#13431)

ericrbg committed 4 years ago

1378eabf

Newer Older