leanprover-community/mathlib

Pull Requests Commits

chore(order/filter/basic): move some parts to new files (#3087)

urkud committed 5 years ago

0736c95c

feat(algebra/category/Algebra): basic setup for category of bundled R-algebras (#3047)

kim-em committed 5 years ago

077cd7c0

feat(algebra/group_action_hom): define equivariant maps (#2866)

kckennylau committed 5 years ago

54441b5d

chore(category_theory/closed): move one thing to monoidal closed and fix naming (#3090)

b-mehta committed 5 years ago

e40de30a

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

leanprover-community-bot committed 5 years ago

a19dca67

feat(topology): sequential compactness (#3061)

PatrickMassot committed 5 years ago

e3c9fd8d

chore(algebra/ring): move `add_mul_self_eq` to `comm_semiring` (#3089)

urkud committed 5 years ago

a478f91b

feat(ring_theory/tensor_product): tensor product of algebras (#3050)

kim-em committed 5 years ago

ae6bf562

feat(analysis/convex): Carathéodory's convexity theorem (#2960)

kim-em committed 5 years ago

a432a3a1

chore(linear_algebra/finite_dimensional): lin-indep lemma typos (#3086)

pechersky committed 5 years ago

b51028f1

feat(linear_algebra/finite_dimensional): bases given by finsets (#3041)

pechersky committed 5 years ago

e0871742

feat(category_theory): cartesian closed categories (#2894)

b-mehta committed 5 years ago

a7960085

feat(tactic/linarith): nlinarith tactic (#2637)

digama0 committed 5 years ago

25e414d1

feat(tactic/group): group normalization tactic (#3062)

PatrickMassot committed 5 years ago

2e752e13

feat(analysis/hofer): Hofer's lemma (#3064)

PatrickMassot committed 5 years ago

aa35f363

chore(linear_algebra/finsupp_vector_space): remove leftover pp.universes (#3081)

gebner committed 5 years ago

4843bb12

feat(linear_algebra/affine_space): more on affine subspaces (#3076)

jsm28 committed 5 years ago

758806ec

feat(field_theory/finite): Chevalley–Warning (#1564)

jcommelin committed 5 years ago

543359ce

feat(polynomial): generalising some material to (noncomm_)semiring (#3043)

kim-em committed 5 years ago

3a66d9ac

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

leanprover-community-bot committed 5 years ago

01732f78

chore(geometry/manifold/real_instances): use euclidean_space (#3077)

sgouezel committed 5 years ago

c91fc150

doc(topology/uniform_space/basic): library note on forgetful inheritance (#3070)

sgouezel committed 5 years ago

c4a32e72

feat(linear_algebra/affine_space): affine combinations of points (#2979)

jsm28 committed 5 years ago

797177c3

perf(*): avoid `user_attribute.get_param` (#3073)

gebner committed 5 years ago

77c5dfe2

chore(data/finset): rename `ext`/`ext'`/`ext_iff` (#3069)

urkud committed 5 years ago

0d052998

refactor(analysis/normed_space/real_inner_product): extend normed_space in the definition (#3060)

sgouezel committed 5 years ago

1f16da1b

perf(tactic/linarith): use key/value lists instead of rb_maps to represent linear expressions (#3004)

robertylewis committed 5 years ago

85b8bdcb

chore(order/basic): move unbundled order classes to `rel_classes (#3066)

urkud committed 5 years ago

7f60a62d

feat(tactic/library_search): small improvements (#3037)

kim-em committed 5 years ago

2c97f239

feat(normed_space/dual): (topological) dual of a normed space (#3021)

hrmacbeth committed 5 years ago

a6534db8

Newer Older