leanprover-community/mathlib3

Pull Requests Commits

chore(analysis/normed_space/bounded_linear_maps): squeeze simps (#17368)

mcdoll committed 3 years ago

a9a490da

chore(linear_algebra/basic): squeeze non-terminal simps (#17367)

mcdoll committed 3 years ago

4bb16a67

chore(data/finsupp/basic): golf a lemma (#17366)

eric-wieser committed 3 years ago

654bbd9c

chore(linear_algebra/basic): add `linear_equiv.conj_apply_apply` (#17364)

eric-wieser committed 3 years ago

fbaa3ad0

chore(data/finsupp): move and rename `finsupp.single_apply_left` (#17357)

Vierkantor committed 3 years ago

34fb08a7

split(algebra/order/nonneg): Separate `ring` and `field` instances (#17348)

YaelDillies committed 3 years ago

43e01caf

can't resist one more

kim-em committed 3 years ago

c089f012

kim-em committed 3 years ago

edcbcecc

Merge branch 'pairwise' into sup

kim-em committed 3 years ago

1e81f661

kim-em committed 3 years ago

efc453b1

kim-em committed 3 years ago

3b7b70e7

Merge branch 'pairwise' into sup

kim-em committed 3 years ago

e84b4a5f

kim-em committed 3 years ago

860787f7

kim-em committed 3 years ago

8a4a6805

kim-em committed 3 years ago

ee4ffa76

kim-em committed 3 years ago

b8872f73

Merge branch 'pnat' into sup

kim-em committed 3 years ago

75e216bb

kim-em committed 3 years ago

7666ffd2

Merge branch 'order_bounds' into sup

kim-em committed 3 years ago

854131e4

fix downstream imports

kim-em committed 3 years ago

6f5557e7

Merge branch 'order_bounds' into sup

kim-em committed 3 years ago

8af4d5ff

fix downstream imports

kim-em committed 3 years ago

4f34e1f9

Merge branch 'order_bounds' into sup

kim-em committed 3 years ago

783aa051

kim-em committed 3 years ago

bbb4c060

fix downstream imports

kim-em committed 3 years ago

225502d8

feat(data/set/basic): add `set.subsingleton_range` (#17248)

urkud committed 3 years ago

d7da6980

refactor(data/set/pairwise): use `{{..}}` arguments (#17230)

urkud committed 3 years ago

00d450eb

feat(data/real/enat_ennreal): define coercion from `enat` to `ennreal` (#17207)

urkud committed 3 years ago

c48d7bfe

refactor(data/fun_like,logic/equiv): generalize instances (#17205)

urkud committed 3 years ago

1b9de287

feat(data/fintype/basic): a type is infinite if it admits an injective map to a proper subset (#17204)

urkud committed 3 years ago

614849cd

Newer Older