leanprover-community/mathlib3

Pull Requests Commits

chore(deprecated/*): Make deprecated classes into structures (#8178)

kbuzzard committed 4 years ago

f961b280

feat(measure_theory/vector_measure): define the pullback and restriction of a vector measure (#8408)

kex-y committed 4 years ago

9ed43801

chore(order/complete_lattice): generalize `Sup_eq_supr'`, add lemmas (#8484)

urkud committed 4 years ago

5b9b4557

feat(order/rel_iso): add `equiv.to_order_iso` (#8482)

urkud committed 4 years ago

de78d424

chore(order/iterate): slightly generalize 2 lemmas (#8481)

urkud committed 4 years ago

4f2006ed

feat(order/partial_sups): complete lattice lemmas (#8480)

YaelDillies committed 4 years ago

2063a528

feat(order/galois_connection): formula for `upper_bounds (l '' s)` (#8478)

urkud committed 4 years ago

79bc7323

feat(data/equiv/mul_add): add `units.coe_inv` (#8477)

urkud committed 4 years ago

4c2edb00

feat(logic/relation): add `*.comap` for `reflexive`, `symmetric`, and `transitive` (#8469)

urkud committed 4 years ago

6c6dd04a

feat(topology/metric_space/holder): add `holder_on_with` (#8454)

urkud committed 4 years ago

0827f3a6

feat(algebra/archimedean): `order_dual α` is archimedean (#8476)

urkud committed 4 years ago

b3943dc0

chore(data/sym): move `data.sym` and `data.sym2` to `data.sym.basic` and `data.sym.sym2` (#8471)

YaelDillies committed 4 years ago

339a122a

doc(analysis/calculus/conformal): fix a docstring (#8479)

justadzr committed 4 years ago

0a480168

feat(data/matrix/basic): update_{column,row}_subsingleton (#8422)

pechersky committed 4 years ago

6e400b90

chore(group_theory/congruence): a few `simp` lemmas (#8452)

urkud committed 4 years ago

977063f6

feat(analysis/normed_space/SemiNormedGroup/kernel): Fix universes + add explicit (#8467)

adamtopaz committed 4 years ago

98b0d18a

feat(algebra/ordered_monoid_lemmas): add one `strict_mono` lemma and a few doc-strings (#8465)

adomani committed 4 years ago

8c89a525

feat(ring_theory): Dedekind domains have invertible fractional ideals (#8396)

Vierkantor committed 4 years ago

a4f16538

feat(logic/unique): unique_of_subsingleton (#8415)

pechersky committed 4 years ago

69e3c79c

doc(data/nat/pairing): fix ascii table markdown (#8460)

gebner committed 4 years ago

7a891508

feat(order/*): a bunch of lemmas about `order_iso` (#8451)

urkud committed 4 years ago

cd6f2720

feat(measure_theory): add @[to_additive] (#8142)

fpvandoorn committed 4 years ago

6d3e9362

ci(bors.toml): add merge-conflict to block_labels (#8455)

bryangingechen committed 4 years ago

870b9d83

feat(ring,group,monoid): map_equiv lemmas for different structures (#8453)

ChrisHughes24 committed 4 years ago

92a5be8d

feat(group_theory/coset): Show that `quotient_group.left_rel` and `left_coset_equivalence` are the same thing (#8382)

eric-wieser committed 4 years ago

7180d2f7

feat(analysis/normed_space/basic): define inclusion `locally_constant X G → C(X, G)` as various types of bundled morphism (#8448)

ocfnash committed 4 years ago

32c82274

feat(algebra/big_operators/basic): add lemmas about prod and sum of finset.erase (#8449)

eric-wieser committed 4 years ago

b71d38ce

feat(data/dfinsupp): add simp lemma `single_eq_zero` (#8447)

eric-wieser committed 4 years ago

0ccd2f66

chore(algebra/floor): add a few trivial `simp` lemmas about `floor` (#8450)

urkud committed 4 years ago

4acfa924

feat(topology/algebra): topological fields (#8316)

PatrickMassot committed 4 years ago

30ff9350

Newer Older