leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into YK-map-prod

urkud committed 3 years ago

5c067289

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

leanprover-community-bot committed 3 years ago

d6a46b79

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

urkud committed 3 years ago

6a5764b3

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

eric-wieser committed 3 years ago

d81cedb1

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

YaelDillies committed 3 years ago

1506335d

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

kmill committed 3 years ago

cbf3062b

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

tb65536 committed 3 years ago

251bd842

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

YaelDillies committed 3 years ago

8bbc5ac4

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

vihdzp committed 3 years ago

fecdd4b2

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

fpvandoorn committed 3 years ago

adfe9c7f

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

urkud committed 3 years ago

936eb7ee

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

BoltonBailey committed 3 years ago

9631a913

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

urkud committed 3 years ago

88ba31c9

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

tb65536 committed 3 years ago

dd34ffaf

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

tb65536 committed 3 years ago

15b764d8

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

tb65536 committed 3 years ago

769ec8c8

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

vihdzp committed 3 years ago

3676f11d

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

javra committed 3 years ago

7bb10813

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

MichaelStollBayreuth committed 3 years ago

2693ab58

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

fpvandoorn committed 3 years ago

eb2780b6

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

ericrbg committed 3 years ago

87f8076f

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

alexjbest committed 3 years ago

dac4f18f

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

ericrbg committed 3 years ago

1378eabf

chore(*): suggestions from the generalisation linter (#13092)

kim-em committed 3 years ago

2249a240

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

leanprover-community-bot committed 3 years ago

a5654710

feat(complex/arg): arg_eq_zero_iff (#13432)

ericrbg committed 3 years ago

b62626e5

chore(order/category/Preorder): reduce imports (#13301)

kim-em committed 3 years ago

0765994d

feat(data/polynomial/*): suggestions from the generalization linter (#13342)

kim-em committed 3 years ago

6f401acf

chore(algebra/polynomial/big_operators): drop some nontrivial assumptions (#13428)

Ruben-VandeVelde committed 3 years ago

76c969b7

feat(model_theory/encoding): Bundled encoding of terms (#13226)

awainverse committed 3 years ago

da13598d

Older