leanprover-community/mathlib3

Pull Requests Commits

A bad start at trying to make norm_fin work on subtraction

eric-wieser committed 4 years ago

5064afa1

fix(order/lattice): make non-instances reducible (#8541)

fpvandoorn committed 4 years ago

3a9b25dd

feat(algebra/opposites): {add,mul,ring}_equiv.op (#8535)

pechersky committed 4 years ago

1691c6c2

refactor(group_theory/solvable): move subgroup commutators into new file (#8534)

kbuzzard committed 4 years ago

096bdb7a

refactor(nat/basic): Move lemma about nat (#8539)

fpvandoorn committed 4 years ago

292e3fa1

feat(topology/discrete_quotient): add two lemmas (#8464)

faenuccio committed 4 years ago

85025718

feat(measure_theory/integration): add some `with_density` lemmas (#8517)

kex-y committed 4 years ago

d366672e

feat(algebra/bounds): a few lemmas like `bdd_above (-s) ↔ bdd_below s` (#8522)

urkud committed 4 years ago

9d129dc2

feat(topology/algebra/ordered/basic): sequences tending to Inf/Sup (#8524)

sgouezel committed 4 years ago

c543ec9a

feat(algebra/floor): notation for nat_floor and nat_ceil (#8526)

sgouezel committed 4 years ago

2b3cffd3

chore(ring_theory/fractional_ideal): make `coe : ideal → fractional_ideal` a `coe_t` (#8529)

Vierkantor committed 4 years ago

1700b3c6

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

Older