leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 4 years ago

812d6bbd

feat(group_theory/sylow): The number of Sylow subgroups equals the index of the normalizer (#9455)

tb65536 committed 4 years ago

125dac81

chore(algebra/category/*): Added `of_hom` to all of the algebraic categories. (#9454)

erdOne committed 4 years ago

b7864434

refactor(algebra/group_with_zero): rename lemmas to use ₀ instead of ' (#9424)

kim-em committed 4 years ago

babca8e3

feat(data/fintype/basic): bijection preserves cardinality (#9473)

tb65536 committed 4 years ago

540fb943

feat(topology/algebra/module): has_continuous_smul (#9468)

PatrickMassot committed 4 years ago

456db24a

chore(topology/algebra): remove dead code (#9467)

PatrickMassot committed 4 years ago

2b23d2eb

chore(measure_theory/decomposition/lebesgue): make measurable_space implicit (#9463)

RemyDegenne committed 4 years ago

5b025712

feat(analysis/normed_space/add_torsor_bases): add lemma `exists_subset_affine_independent_span_eq_top_of_open` (#9418)

ocfnash committed 4 years ago

a24b4965

feat(data/set/equitable): Equitable functions (#8509)

YaelDillies committed 4 years ago

931cd6d7

chore(analysis/convex/basic): instance cleanup (#9466)

YaelDillies committed 4 years ago

a52a54b6

feat(measure_theory/constructions/pi): volume on `α × α` as a map of volume on `fin 2 → α` (#9432)

urkud committed 4 years ago

97036e7c

feat(order/succ_pred): define successor orders (#9397)

YaelDillies committed 4 years ago

64bcb389

feat(monoid_algebra/grading): `add_monoid_algebra`s permit an internal grading (#8927)

eric-wieser committed 4 years ago

f7795d1a

feat(linear_algebra/affine_space/combination): add lemma `finset.map_affine_combination` (#9453)

ocfnash committed 4 years ago

b18eedb0

move(category_theory/category/default): rename to `category_theory.basic` (#9412)

YaelDillies committed 4 years ago

6e6fe1f2

refactor(linear_algebra/free_module): split in two files (#9407)

riccardobrasca committed 4 years ago

4091f72b

feat(*): Clean up some misstated lemmas about analysis/manifolds (#9395)

alexjbest committed 4 years ago

6210d98a

refactor(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic (#9331)

eric-wieser committed 4 years ago

118e809b

feat(data/(d)finsupp): update_eq_sub_add_single (#9184)

pechersky committed 4 years ago

0dca20a2

feat(ring_theory/henselian): Henselian local rings (#8986)

jcommelin committed 4 years ago

8ec7fcf8

feat(group_theory/perm/concrete_cycle): perm.to_list (#9178)

pechersky committed 4 years ago

f184dd7d

refactor(algebra/abs): add has_abs class (#9172)

mans0954 committed 4 years ago

3daae2ca

chore(order/basic): rename monotonicity concepts (#9383)

YaelDillies committed 4 years ago

2fd713a7

feat(ring_theory/finiteness): add finiteness of restrict_scalars (#9363)

riccardobrasca committed 4 years ago

09506e6c

docs(category_theory): provide missing module docs (#9352)

kim-em committed 4 years ago

3b48f7a5

feat(group_theory/complement): Top is complement to every singleton subset (#9460)

tb65536 committed 4 years ago

6d12b2e1

chore(linear_algebra/quadratic_form): add missing lemmas, lift instance, and tweak argument implicitness (#9458)

eric-wieser committed 4 years ago

f31758a8

feat(set_theory/cardinal_ordinal): there is no injective function from ordinals to types in the same universe (#9452)

sgouezel committed 4 years ago

f6d2434f

feat(algebra/star): If `R` is a `star_monoid`/`star_ring` then so is `Rᵒᵖ` (#9446)

eric-wieser committed 4 years ago

089614b1

Newer Older