leanprover-community/mathlib

Pull Requests Commits

Merge commit '5afd09aace106e3160dacca2484e15e74f35ab7c' into eric-wieser/remove-matrix-scalar

eric-wieser committed 4 years ago

9f4b19cf

move bundled versions

eric-wieser committed 4 years ago

62fc900a

refactor(data/matrix/basic): Remove matrix.scalar

eric-wieser committed 4 years ago

dfcf4aa2

chore(data/matrix/basic): move bundled versions of `matrix.map` beneath the algebra structure (#8528)

eric-wieser committed 4 years ago

5afd09aa

feat(order/bounds): add `is_lub_pi` and `is_glb_pi` (#8521)

urkud committed 4 years ago

3f4b8368

feat(fractional_ideal): `coe : ideal → fractional_ideal` as ring hom (#8511)

Vierkantor committed 4 years ago

ad83714b

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

Older