leanprover-community/mathlib

Pull Requests Commits

hrmacbeth committed 3 years ago

0a900220

instances to defs

hrmacbeth committed 3 years ago

bbf1d24c

normed_space.basc

hrmacbeth committed 3 years ago

5e464bf7

normed.group.basic

hrmacbeth committed 3 years ago

ef02c849

metric_space.lipschitz

hrmacbeth committed 3 years ago

a897ccec

hrmacbeth committed 3 years ago

448c0b4a

feat(data/finsupp/basic): lemmas about map domain with only inj_on hypotheses (#11484)

alexjbest committed 3 years ago

7ee41aab

chore(*): clean up comment strings in docstrings (#11557)

alexjbest committed 3 years ago

bbd0f769

feat(data/finset/slice): More `finset.slice` and antichain lemmas (#11397)

YaelDillies committed 3 years ago

a90f9692

feat(data/sum/interval): The disjoint sum of two locally finite orders is locally finite (#11351)

YaelDillies committed 3 years ago

c72e709e

feat(algebra/roots_of_unity): basic constructor (#11504)

ericrbg committed 3 years ago

dbf59ba1

chore(algebra/algebra): algebra_map_int_eq (#11474)

ericrbg committed 3 years ago

7ddaf104

chore(algebra/order/sub): Generalize to `preorder` and `add_comm_semigroup` (#11463)

YaelDillies committed 3 years ago

4ad74aed

feat(analysis/normed/group/pointwise): the closed thickening of a compact set is the addition of a closed ball. (#11528)

sgouezel committed 3 years ago

1cfb97d5

feat(category_theory/bicategory/locally_discrete): define locally discrete bicategory (#11402)

yuma-mizuno committed 3 years ago

ff9b7574

feat(measure_theory/measure/measure_space): better definition of to_measurable (#11529)

sgouezel committed 3 years ago

6dd65257

feat(data/nat/factorization): add two convenience lemmas (#11543)

stuart-presnell committed 3 years ago

de53f9c4

feat(linear_algebra,algebra,group_theory): miscellaneous lemmas linking some additive monoid and module operations (#11525)

eric-wieser committed 3 years ago

5a1cbe36

feat(ring_theory/norm): add is_integral_norm (#11489)

riccardobrasca committed 3 years ago

a0ff65df

feat(ring_theory/graded_algebra/basic): add a helper for construction from an alg hom (#11541)

eric-wieser committed 3 years ago

6f23973a

feat(measure_theory): generalize `null_of_locally_null` to `outer_measure`, add versions (#11535)

urkud committed 3 years ago

496a744e

feat(topology/separation): add `t1_space_tfae` (#11534)

urkud committed 3 years ago

be9a5dec

feat(data/set): two simple lemmas (#11531)

sgouezel committed 3 years ago

135a92d1

feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515)

ocfnash committed 3 years ago

5bbc187e

feat(algebra/big_operators/basic): Reindexing a product with a permutation (#11344)

YaelDillies committed 3 years ago

a0da4f1f

chore(order/bounded_order): golf (#11538)

urkud committed 3 years ago

8d5caba3

feat(measure_theory): drop some `measurable_set` assumptions (#11536)

urkud committed 3 years ago

a217b9c3

chore(algebra/order/ring): move lemmas about invertible into a new file (#11511)

eric-wieser committed 3 years ago

f23c00f2

feat(data/fintype/basic): `one_lt_card_iff` and `two_lt_card_iff` (#11524)

tb65536 committed 3 years ago

01fa7f52

chore(cone_category): generalize universes (#11539)

alreadydone committed 3 years ago

e895c8fa

Older