leanprover-community/mathlib

Pull Requests Commits

chore(topology/maps): golf, use section vars (#10747)

urkud committed 4 years ago

563c3643

feat(archive/imo): IMO 2005 problem 4 (modular arithmetic) (#10746)

hrmacbeth committed 4 years ago

10fb7f91

split(data/set/prod): split off `data.set.basic` (#10739)

YaelDillies committed 4 years ago

9d73418c

feat(linear_algebra/orientation): inherit an action by `units R` on `module.ray R M` (#10738)

eric-wieser committed 4 years ago

e60899c5

refactor(algebra/triv_sq_zero_ext): generalize and cleanup (#10729)

eric-wieser committed 4 years ago

ea88bd61

feat(data/{list, multiset, finset}/range): add range_add (#10706)

BoltonBailey committed 4 years ago

e70e22f2

feat(order/galois_connection): add lt_iff_lt (#10702)

BoltonBailey committed 4 years ago

e4b6b5cc

feat(data/polynomial/degree/definitions): add pow lemmas (#10698)

greysome committed 4 years ago

29fecae5

feat(analysis/convex/basic): lemmas about midpoint and segment (#10682)

ADedecker committed 4 years ago

fb819501

feat(algebra/graded_monoid): dependent products (#10674)

eric-wieser committed 4 years ago

f8171e09

feat(*): Random lemmas about adjoin/span. (#10666)

erdOne committed 4 years ago

309da201

feat(algebra/pointwise): Multiplying a singleton (#10660)

YaelDillies committed 4 years ago

e19473a9

feat(analysis/convex/strict): Strictly convex sets (#10648)

YaelDillies committed 4 years ago

ec48e3b9

feat(ring_theory/polynomial/cyclotomic/*): ɸₙ(1) = 1 (#10483)

ericrbg committed 4 years ago

2d47c1d6

chore(category_theory/limits): Generalize universe for preserving limits (#10736)

erdOne committed 4 years ago

7cd8adb7

feat(algebraic_geometry): An integral scheme is reduced and irreducible (#10733)

erdOne committed 4 years ago

381b9541

feat(data/mv_polynomial/variables): API for mv_polynomial.degree_of (#10646)

isadofschi committed 4 years ago

214a80f3

feat(category_theory/limits): The associativity of pullbacks and pushouts. (#10619)

erdOne committed 4 years ago

8b8f08d0

feat(algebraic_geometry/presheafed_space): Open immersions of presheafed spaces has pullbacks. (#10069)

erdOne committed 4 years ago

b6b47ed5

feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735)

erdOne committed 4 years ago

fcd0f11c

feat(data/nat/prime): add `prime.dvd_mul_of_dvd_ne` (#10727)

stuart-presnell committed 4 years ago

06905422

feat(algebra/{group,ring}/opposite): `{ring,monoid}_hom.from_opposite` (#10723)

eric-wieser committed 4 years ago

0c248b74

chore(algebra/module/submodule): missing is_central_scalar instance (#10720)

eric-wieser committed 4 years ago

4b079496

feat(algebra/tropical/big_operators): sum, prod, Inf (#10544)

pechersky committed 4 years ago

41def6a8

chore(linear_algebra/orientation): golf a proof (#10742)

eric-wieser committed 4 years ago

b9f24408

chore(tactic/reserved_notation): change precedence of sup and inf (#10623)

RemyDegenne committed 4 years ago

19dd4be3

refactor(data/{mv_,}polynomial): lemmas about `adjoin` (#10670)

urkud committed 4 years ago

61b0f419

move(data/bool/*): Move `bool` files in one folder (#10718)

YaelDillies committed 4 years ago

e68fcf8d

feat(algebra/order/ring): pos_iff_pos_of_mul_pos, neg_iff_neg_of_mul_pos (#10634)

jsm28 committed 4 years ago

50e318ec

chore(order/boolean_algebra): add `compl_sdiff` (#10722)

urkud committed 4 years ago

f3613738

Newer Older