leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569)

joelriou committed 3 years ago

31019c25

feat(algebra/order/group/defs): add choice-free shortcut instances for `ordered_comm_group` (#17564)

astrainfinita committed 3 years ago

011aebd9

doc(tactic/congr): add relationship to `move_add` in `ac_change` (#14618)

adomani committed 3 years ago

28b66e1a

feat(topology/algebra/module/finite_dimension): `can_lift` instances (#17773)

YaelDillies committed 3 years ago

246853d5

feat(quiver/basic): push arrows of a quiver along a map (#17618)

bottine committed 3 years ago

7ba713a7

chore(algebra/star/basic): split out `big_operators` import (#17792)

hrmacbeth committed 3 years ago

6f6739f8

chore(data/set/pointwise/basic): split (#17768)

hrmacbeth committed 3 years ago

9114ddff

feat({data/finset/basic, ring_theory/roots_of_unity, algebra/ring/units}): add lemmas (#17671)

riccardobrasca committed 3 years ago

084ba5e0

chore(measure_theory/measurable_space_def): delete unused import (#17799)

hrmacbeth committed 3 years ago

94c141ac

feat(data/polynomial/basic): add to_finsupp_C_mul_X_pow lemmas (#17794)

Multramate committed 3 years ago

e574b1a4

chore(*): add mathlib4 synchronization comments (#17790)

github-actions[bot] committed 3 years ago

308f6d03

chore(data/real/cau_seq): generalize to noncommutative settings (#17785)

eric-wieser committed 3 years ago

e469260a

feat(algebra/group/pi): add pi.monoid_hom (#17757)

xroblot committed 3 years ago

76658a41

feat(geometry/manifold/smooth_manifold_with_corners): define local_homeomorph.extend (#17669)

fpvandoorn committed 3 years ago

a1ce0bd9

feat(data/real/cau_seq): downgrade a proof (#17791)

hrmacbeth committed 3 years ago

e5178d62

fix(scripts/port_status): do not list sync-comment-only diffs (#17788)

eric-wieser committed 3 years ago

6d582e0f

fix(scripts/add_port_comments): make message insertion less fragile (#17756)

eric-wieser committed 3 years ago

462d96e5

feat(measure_theory/integral/bochner): continuity statements within a set for integrals (#17625)

sgouezel committed 3 years ago

4b2336ec

chore(algebra/order/group/defs): split file (#17787)

kim-em committed 3 years ago

4bcba0da

chore(data/set/function): two trivial lemmas (#17784)

eric-wieser committed 3 years ago

1c9ea256

feat(algebraic_topology/dold_kan): the normalized Moore complex of a split simplicial object (#17548)

joelriou committed 3 years ago

50cbd1a0

refactor(algebra/group_ring_action): split out subobject actions (#17786)

eric-wieser committed 3 years ago

afad8e43

chore(algebra/char_zero): split (#17760)

hrmacbeth committed 3 years ago

70d50ecf

chore(algebra/ring/equiv): split out results about big operators (#17750)

Ruben-VandeVelde committed 3 years ago

5cd3c253

feat(geometry/euclidean/angle/oriented/affine): equidistant points and `π / 2` rotations (#17722)

jsm28 committed 3 years ago

35da8bde

feat(analysis/special_functions/trigonometric/angle): absolute value lemmas (#17485)

jsm28 committed 3 years ago

f9c5995b

feat(geometry/euclidean/triangle): oangle_add_oangle_add_oangle_eq_pi (#17781)

eric-wieser committed 3 years ago

e9d89fee

chore(*): add mathlib4 synchronization comments (#17754)

github-actions[bot] committed 3 years ago

8d89a80d

feat(linear_algebra/affine_space/affine_subspace): `affine_span_pair` inequality lemmas (#17636)

jsm28 committed 3 years ago

0e86ecbb

chore(data/countable/defs): add explanation of nolint (#17732)

kim-em committed 3 years ago

49b1e35c

Newer Older