leanprover-community/mathlib

Pull Requests Commits

feat(analysis/convex/basic): convex hull and empty set (#7232)

b-mehta committed 4 years ago

b2e7f40f

doc(group_theory): fix `normalizer` docstring (#7231)

mguaypaq committed 4 years ago

22924634

feat(data/equiv/mul_add): use `@[simps]` (#7213)

fpvandoorn committed 4 years ago

21d74c7a

feat(data/nat/choose/sum): Add lower bound lemma for central binomial coefficient (#7214)

BoltonBailey committed 4 years ago

9363a649

feat(analysis/normed_space/operator_norm): generalize to seminormed space (#7202)

riccardobrasca committed 4 years ago

e9a11f6e

chore(category_theory/subobject): different proof of le_of_comm (#7229)

TwoFX committed 4 years ago

206ecce7

feat(order/conditionally_complete_lattice): conditional Inf of intervals (#7226)

b-mehta committed 4 years ago

0f6c1f19

feat(category_theory): formally adjoined initial objects are strict (#7222)

TwoFX committed 4 years ago

560a0092

chore(ring_theory/adjoin.basic): use submodule.closure in algebra.adjoin_eq_span (#7194)

riccardobrasca committed 4 years ago

89c16a79

feat(test/integration): improve an example (#7169)

benjamindavidson committed 4 years ago

b7a3d4e1

feat(category_theory/triangulated/pretriangulated): add definition of pretriangulated categories and triangulated functors between them (#7153)

l-kershaw committed 4 years ago

6b182fcd

feat(data/list/basic): fold[rl] recursion principles (#7079)

pechersky committed 4 years ago

110541dd

feat(data/set): sep true/false simp lemmas (#7215)

b-mehta committed 4 years ago

49040e50

feat(data/finsupp/basic): add finsupp.single_left_injective and docstrings (#7207)

eric-wieser committed 4 years ago

24013e2b

feat(order/rel_iso): constructors for rel embeddings (#7046)

b-mehta committed 4 years ago

06886125

feat(category_theory): the additive envelope, Mat_ C (#6845)

kim-em committed 4 years ago

ea4dce03

chore(algebra): add `sub{_mul_action,module,semiring,ring,field,algebra}.copy` (#7220)

eric-wieser committed 4 years ago

108b9235

chore(group_theory/subgroup): rename `monoid_hom.to_range` to `monoid_hom.range_restrict` (#7218)

eric-wieser committed 4 years ago

e00d688f

chore(data/mv_polynomial/basic): golf some proofs (#7209)

eric-wieser committed 4 years ago

b1acb58a

feat(data/multiset/basic): some multiset lemmas, featuring sum inequalities (#7090)

awainverse committed 4 years ago

bb9b850e

feat(category_theory/kernels): missing instances (#7204)

kim-em committed 4 years ago

148760e3

refactor(category_theory/images): improvements (#7198)

kim-em committed 4 years ago

9d1ab69f

doc(topology/bases): add module + theorem docstrings (#7193)

ericrbg committed 4 years ago

81b8873e

fix(.github/PULL_REQUEST_TEMPLATE.md): revert gitpod button URL (#7210)

bryangingechen committed 4 years ago

8742be7c

doc(tactic/congr): example where congr fails, but exact works (#7208)

gebner committed 4 years ago

37ab34ea

chore(group/ring_hom): fix a nat nsmul diamond (#7201)

sgouezel committed 4 years ago

b4201e7b

chore(algebra/module/submodule): add missing coe lemmas (#7205)

eric-wieser committed 4 years ago

50a843e0

feat(linear_algebra/basic): add span_eq_add_submonoid.closure (#7200)

riccardobrasca committed 4 years ago

14c625e1

feat(number_theory/bernoulli): golf (#7197)

benjamindavidson committed 4 years ago

0f3ca672

chore(topology/vector_bundle): generalize to topological semimodules (#7183)

urkud committed 4 years ago

6a4d298c

Newer Older