leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 4 years ago

43c9be02

feat(group_theory/perm/concrete_cycle): computable cyclic perm notation (#9470)

pechersky committed 4 years ago

7ed091df

chore(analysis/normed_space/linear_isometry): adjust `isometry` API (#9635)

hrmacbeth committed 4 years ago

ce50450d

feat(order/min_max): min_cases and max_cases lemmata (#9632)

AlexKontorovich committed 4 years ago

a9643aa8

feat(analysis/convex/quasiconvex): Quasiconvexity of functions (#9561)

YaelDillies committed 4 years ago

e0f80e78

refactor(data/nat/basic): finish removing sub lemmas (#9601)

fpvandoorn committed 4 years ago

7a7fadaf

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

leanprover-community-bot committed 4 years ago

7aaa1b43

chore(*): fix typos (#9634)

Ruben-VandeVelde committed 4 years ago

7e3fa4c1

refactor(group_theory/monoid_localization) remove old_structure_cmd (#9621)

kim-em committed 4 years ago

70a9540d

refactor(field_theory/intermediate_field): remove old_structure_cmd (#9620)

kim-em committed 4 years ago

c37e3e79

refactor(algebra/lie): reduce use of old_structure_cmd (#9616)

kim-em committed 4 years ago

b39feab3

chore(data/equiv/ring): add big operator lemmas for ring equivs (#9628)

dupuisf committed 4 years ago

91ee8f1d

feat(analysis/normed_space/exponential): remove char_p assumption (#9618)

ADedecker committed 4 years ago

57cd1e9e

feat(algebra/graded_monoid): Split out graded monoids from graded rings (#9586)

eric-wieser committed 4 years ago

5fd36643

feat(data/polynomial): %ₘ as a linear map (#9532)

Vierkantor committed 4 years ago

745cbfc6

refactor(geometry/manifold): remove old_structure_cmd (#9617)

kim-em committed 4 years ago

99c3e223

refactor(ring_theory/valuation): remove unnecessary old_structure_cmd (#9615)

kim-em committed 4 years ago

c107549d

refactor(order/category): remove old_structure_cmd (#9614)

kim-em committed 4 years ago

7bdd10e2

refactor(algebra/absolute_value): remove unnecessary old_structure_cmd (#9613)

kim-em committed 4 years ago

af09d3ff

refactor(order/omega_complete_partial_order): remove old_structure_cmd (#9612)

kim-em committed 4 years ago

25a45ab7

feat(*): add not_mem_of_not_mem_closure for anything with subset_closure (#9595)

alexjbest committed 4 years ago

cea97d9a

refactor(data/finsupp/basic): remove sub lemmas (#9603)

fpvandoorn committed 4 years ago

6c9eee4b

feat(group_theory/subgroup/basic): a new to_additive lemma, and remove a by hand proof (#9594)

alexjbest committed 4 years ago

34145b7f

feat(ring_theory): `adjoin_root g ≃ S` if `S` has a power basis with the right minpoly (#9529)

Vierkantor committed 4 years ago

d5146f4e

feat(ring_theory): generalize `power_basis.equiv` (#9528)

Vierkantor committed 4 years ago

82e2b98a

feat(algebra/star/algebra): generalize to modules (#9484)

eric-wieser committed 4 years ago

179a4952

chore(algebra/order/sub): generalize 2 lemmas (#9611)

urkud committed 4 years ago

9ecdd380

feat(algebra/order/ring): variants of mul_sub' (#9604)

fpvandoorn committed 4 years ago

639a7ef4

feat(data/nat/log): add antitonicity lemmas for first argument (#9597)

jchoules committed 4 years ago

83a07ce0

feat(data/multiset/interval): Intervals as `multiset`s (#9588)

YaelDillies committed 4 years ago

41dd4da3

Older