leanprover-community/mathlib

Pull Requests Commits

feat(data/finset/basic): Add `coe_pair` lemmas (#16235)

linesthatinterlace committed 3 years ago

8d90fcdb

chore(data/real/nnreal): Golf (#16307)

YaelDillies committed 3 years ago

370cc484

feat(data/sign): Allocating signs (#14335)

YaelDillies committed 3 years ago

616e6ef3

refactor(topology/algebra/continuous_monoid_hom): Make variables consistent (#16304)

tb65536 committed 3 years ago

9b68ed5e

feat(*): bump to lean 3.48.0 (#16292)

gebner committed 3 years ago

acbe099c

doc(measure_theory/integral): integrability docstrings (#16269)

mcdoll committed 3 years ago

87d8c4b3

chore(algebra/divisibility): golf (#16327)

astrainfinita committed 3 years ago

371b4143

refactor(group_theory/subgroup/basic): Make `subgroup.opposite` an `equiv` (#16271)

YaelDillies committed 3 years ago

5b7bc676

feat(probability/independence): add indep_bot_left and indep_bot_right (#16309)

RemyDegenne committed 3 years ago

39014ec9

feat(order/filter/small_sets): yet another squeeze theorem (#16286)

urkud committed 3 years ago

5a3cd16b

feat(algebra/invertible): `map_inv_of` and some other basic results (#16202)

eric-wieser committed 3 years ago

5e194d48

chore(algebra/order/absolute_value): superficial tidying (#16190)

ericrbg committed 3 years ago

76be8c73

feat(topology/sheaves/sheaf_condition): Description of sections on the union of two open sets. (#16093)

erdOne committed 3 years ago

27d83241

feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete (#15988)

TwoFX committed 3 years ago

361aa777

feat(linear_algebra/affine_space/finite_dimensional): `insert` lemmas (#16308)

jsm28 committed 3 years ago

865184b4

chore(topology/instances/rat): add `namespace rat` (#16306)

urkud committed 3 years ago

07190764

feat(logic/equiv/option): equivalence with subtypes (#16302)

jsm28 committed 3 years ago

1e91718f

refactor(analysis/convex/cone): move cone.lean to cone/basic.lean (#16270)

apurvnakade committed 3 years ago

d44692a8

feat(algebra/gcd_monoid): `simp` lemmas for `associated (normalize x) y` (#16249)

Vierkantor committed 3 years ago

2d30ffcf

feat(algebra/order/smul): `ordered_smul` instances for `ℕ` and `ℤ` (#16247)

YaelDillies committed 3 years ago

eaa51e72

feat(algebraic_topology/dold_kan): the normalized Moore complex is homotopy equivalent to the alternating face map complex (#16246)

joelriou committed 3 years ago

f951e201

feat(algebra/category/Module/change_of_rings): extension of scalars (#15673)

jjaassoonn committed 3 years ago

9e274549

chore(algebra/regular/basic): clean up variables and slight golf (#16321)

adomani committed 3 years ago

f84386d7

feat(topology/instances/ennreal): `ennreal.to_nnreal` applied to a `tsum` (#16320)

dtumad committed 3 years ago

17ff82d9

feat(logic/basic): `function.mt` and `function.mtr` (#16315)

kmill committed 3 years ago

b35461b8

chore(topology/algebra/order/basic): deduplicate (#16287)

urkud committed 3 years ago

6a68f86a

feat(order/locally_finite): transfer locally_finite_order across order_iso (#16264)

gebner committed 3 years ago

386acbac

feat(data/finset/locally_finite): more on `filter (< c)` (#16260)

gebner committed 3 years ago

70c48638

refactor(algebra/monoid_algebra/{ basic + support } + import dust): move lemmas to a new "support" file (#16322)

adomani committed 3 years ago

20cfd341

feat(analysis/complex/basic): add `complex.ring_hom_eq_id_or_conj_of_continuous` (#16169)

xroblot committed 3 years ago

489c1c57

Newer Older