leanprover-community/mathlib3

Pull Requests Commits

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)

leanprover-community-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

feat(algebraic_topology/dold_kan): starting the definition of the inverse functor of the Dold-Kan equivalence (#17551)

joelriou committed 3 years ago

369b22a4

feat(algebraic_geometry): Qcqs lemma (#15996)

erdOne committed 3 years ago

94625350

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

leanprover-community-bot committed 3 years ago

6eb334bd

chore(algebra/module/basic): remove dependency on finiteness (#17764)

hrmacbeth committed 3 years ago

94825b2b

feat(combinatorics/additive/energy): Additive energy (#17734)

YaelDillies committed 3 years ago

7080d596

feat(measure_theory/group/measure): Mapping an Haar measure under a linear iso (#17771)

YaelDillies committed 3 years ago

1d4a2038

chore(group_theory/sub*): avoid fintype dependencies (#17762)

Ruben-VandeVelde committed 3 years ago

56c7bf86

feat(algebra/order/interval): Interval arithmetic (#16761)

YaelDillies committed 3 years ago

1a513788

refactor(data/nat/basic): move more bit theory out (#17763)

kim-em committed 3 years ago

7ac96dea

chore(data/real/ereal): fix addition and multiplication on ereal (#17770)

sgouezel committed 3 years ago

83871f6c

chore(measure_theory/group/fundamental_domain: Generalise to two groups (#17766)

YaelDillies committed 3 years ago

7bf99266

chore(number_theory/modular_forms/slash_invariant_forms): deduplicate scalar actions (#17765)

eric-wieser committed 3 years ago

1c67b653

chore(linear_algebra/basic): golf a lemma statement (#17752)

eric-wieser committed 3 years ago

ca95e36a

Newer Older