leanprover-community/mathlib

Pull Requests Commits

chore(data/finset): minor review (#3105)

urkud committed 6 years ago

24792be6

fix(tactic/linarith): don't fail trying to preprocess irrelevant hypotheses (#3104)

robertylewis committed 6 years ago

eb5b7fb7

chore(category_theory/closed/cartesian): style (#3098)

kim-em committed 6 years ago

b91909e7

feat(algebra/linear_ordered_comm_group_with_zero) define linear_ordered_comm_group_with_zero (#3072)

kckennylau committed 6 years ago

b5baf555

refactor(measure_theory): make `volume` a bundled measure (#3075)

urkud committed 6 years ago

48c4f400

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

urkud committed 6 years ago

0736c95c

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

kim-em committed 6 years ago

077cd7c0

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

kckennylau committed 6 years ago

54441b5d

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

b-mehta committed 6 years ago

e40de30a

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

leanprover-community-bot committed 6 years ago

a19dca67

feat(topology): sequential compactness (#3061)

PatrickMassot committed 6 years ago

e3c9fd8d

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

urkud committed 6 years ago

a478f91b

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

kim-em committed 6 years ago

ae6bf562

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

kim-em committed 6 years ago

a432a3a1

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

pechersky committed 6 years ago

b51028f1

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

pechersky committed 6 years ago

e0871742

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

b-mehta committed 6 years ago

a7960085

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

digama0 committed 6 years ago

25e414d1

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

PatrickMassot committed 6 years ago

2e752e13

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

PatrickMassot committed 6 years ago

aa35f363

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

gebner committed 6 years ago

4843bb12

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

jsm28 committed 6 years ago

758806ec

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

jcommelin committed 6 years ago

543359ce

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

kim-em committed 6 years ago

3a66d9ac

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

leanprover-community-bot committed 6 years ago

01732f78

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

sgouezel committed 6 years ago

c91fc150

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

sgouezel committed 6 years ago

c4a32e72

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

jsm28 committed 6 years ago

797177c3

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

gebner committed 6 years ago

77c5dfe2

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

urkud committed 6 years ago

0d052998

Newer Older