leanprover-community/mathlib3

Pull Requests Commits

chore(gitpod): be slightly more intelligent about getting a PR cache

eric-wieser committed 4 years ago

Verified fe69dea0

chore(order/bounds): add `@[simp]` attrs, add `not_bdd_*_univ` (#8520)

urkud committed 4 years ago

b681b6b9

feat(algebra/ordered_monoid): a few more `order_dual` instances (#8519)

urkud committed 4 years ago

10216790

feat(algebra/group_with_zero): pullback a `comm_cancel_monoid_with_zero` instance across an injective hom (#8515)

Vierkantor committed 4 years ago

0bef4a0b

feat(data/matrix/basic): Add bundled versions of matrix.diagonal (#8510)

eric-wieser committed 4 years ago

2568d41b

feat(simps): better name for additivized simps-lemmas (#8457)

fpvandoorn committed 4 years ago

77d6c8e8

chore(data/matrix): delete each of the `matrix.foo_hom_map_zero` (#8512)

Vierkantor committed 4 years ago

17f1d28c

feat(data/equiv/mul_add): add `equiv.(div,sub)_(left,right)` (#8385)

eric-wieser committed 4 years ago

17b1e7ce

refactor(data/matrix/basic): merge duplicate algebra structures (#8486)

eric-wieser committed 4 years ago

9a251f1e

feat(algebra/ordered_monoid): add_eq_bot_iff (#8474)

pechersky committed 4 years ago

c8b7816d

feat(order/bounded_lattice): add some disjoint lemmas (#8407)

kex-y committed 4 years ago

f354c1b1

docs(overview): add holder continuity (#8506)

urkud committed 4 years ago

af8e56af

chore(data/real/basic): cleanup (#8501)

urkud committed 4 years ago

25a42309

chore(data/int): move some lemmas from `basic` to a new file (#8495)

urkud committed 4 years ago

69c6adb5

feat(data/matrix/basic): provide equiv versions of `matrix.map`, `linear_map.map_matrix`, and `ring_hom.map_matrix`. (#8468)

eric-wieser committed 4 years ago

4a9cbdb1

feat(group_theory/coset): card_dvd_of_injective (#8485)

ChrisHughes24 committed 4 years ago

1b771af7

refactor(data/real/nnreal): use `ord_connected_subset_conditionally_complete_linear_order` (#8502)

urkud committed 4 years ago

0f168d3e

feat(algebra/group_power/lemmas): is_unit_pos_pow_iff (#8420)

pechersky committed 4 years ago

5994df14

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

leanprover-community-bot committed 4 years ago

db0cd4db

doc(algebra/algebra/basic): add a comment to make the similar definition discoverable (#8500)

eric-wieser committed 4 years ago

bfa6bbbc

feat(algebra/group/semiconj): add `semiconj_by.reflexive` and `semiconj_by.transitive` (#8493)

urkud committed 4 years ago

fdb0369f

feat(algebra/ordered_group): add `order_iso.inv` (#8492)

urkud committed 4 years ago

60c378d0

feat(group_theory/congruence): add `con.lift_on_units` etc (#8488)

urkud committed 4 years ago

1530d767

feat(group_theory/order_of_element): order_of_dvd_iff_gpow_eq_one (#8487)

ChrisHughes24 committed 4 years ago

9c4dd02d

feat(data/nat/prime): pow_dvd_of_dvd_mul_right (#8483)

ChrisHughes24 committed 4 years ago

9194f20c

feat(group_theory/subgroup): add `subgroup.forall_gpowers` etc (#8470)

urkud committed 4 years ago

b0991037

chore(algebra/group/hom_instances): add monoid_hom versions of linear_map lemmas (#8461)

eric-wieser committed 4 years ago

52a2e8b9

feat(data/nat/totient): totient_prime_pow (#8353)

ChrisHughes24 committed 4 years ago

894fb0c5

feat(measure_theory/[integrable_on, set_integral]): integrals on two ae-eq sets are equal (#8440)

ADedecker committed 4 years ago

7249afb2

refactor(data/set/lattice): add congr lemmas for `Prop`-indexed `Union` and `Inter` (#8260)

urkud committed 4 years ago

d3c943b7

Older