leanprover-community/mathlib

Pull Requests Commits

fix(algebra/ring_quot): fix a diamond in the int-smul action (#14226)

eric-wieser committed 4 years ago

a5f4cf53

refactor(*): `insert_singleton` → `pair` (#14210)

vihdzp committed 4 years ago

32700f50

feat(linear_algebra/trace): trace of tensor_products and hom_tensor_hom is an equivalence (#13728)

antoinelab01 committed 4 years ago

5fe43a91

doc(src/deprecated/*): add module docstrings (#14224)

kbuzzard committed 4 years ago

259c951d

feat(data/set/basic): add `set.subset_range_iff_exists_image_eq` and `set.range_image` (#14203)

urkud committed 4 years ago

4f31117e

chore(analysis,topology): add missing ulift instances (#14217)

eric-wieser committed 4 years ago

470ddbdb

chore(data/fintype/basic): Better `fin` lemmas (#14200)

YaelDillies committed 4 years ago

503970d2

feat(analysis/convex/combination): The convex hull of `s + t` (#14160)

YaelDillies committed 4 years ago

c38ab356

feat(ring_theory/ideal/operations.lean): lemmas about coprime ideals (#14176)

pbazin committed 4 years ago

cfedf1d5

refactor(data/list/min_max): Generalise `list.argmin`/`list.argmax` to preorders (#13221)

MantasBaksys committed 4 years ago

2c2d515a

feat(topology/algebra/module/multilinear): add `continuous_multilinear_map.smul_right` (#14218)

ADedecker committed 4 years ago

54773fc0

feat(logic/lemmas): Distributivity of `if then else` (#14146)

YaelDillies committed 4 years ago

9dc9c3ea

feat(linear_algebra/multilinear/finite_dimensional): generalize to finite and free (#14199)

eric-wieser committed 4 years ago

ae6a7c3f

chore(data/multiset/basic): `∅` → `0` (#14211)

vihdzp committed 4 years ago

59facea4

chore(measure_theory/function/strongly_measurable): golf some proofs (#14209)

urkud committed 4 years ago

d08f7340

chore(data/multiset/basic): Inline instances (#14208)

vihdzp committed 4 years ago

50696a85

feat(data/polynomial/mirror): Central coefficient of `p * p.mirror` (#14096)

tb65536 committed 4 years ago

9f6f605b

feat(category_theory/limits): reindexing (co/bi)products (#14193)

kim-em committed 4 years ago

f48cbb16

feat(data/multiset/basic): `pair_comm` (#14207)

vihdzp committed 4 years ago

ca5930df

feat(analysis/special_functions/trigonometric/arctan): add `real.range_arctan` (#14204)

urkud committed 4 years ago

6b291d7b

feat(analysis/normed_space/M_structure): Define L-projections, show they form a Boolean algebra (#12173)

mans0954 committed 4 years ago

632fef37

refactor(algebra/parity): Generalize to division monoids (#14187)

YaelDillies committed 4 years ago

0afb90b4

feat(topology/instances/matrix): add topological/continuous instances (#14202)

aronerben committed 4 years ago

21581937

chore(linear_algebra/multilinear/basic): move finite-dimensionality to a new file (#14198)

eric-wieser committed 4 years ago

1f0f9813

feat(analysis/locally_convex/with_seminorms): pull back `with_seminorms` along a linear inducing (#13549)

ADedecker committed 4 years ago

ae6f59d7

feat(group_theory/perm/list): Add missing `form_perm` lemmas (#13218)

MantasBaksys committed 4 years ago

ba38b47f

chore(set_theory/ordinal/{basic, arithmetic}): Inline instances (#14076)

vihdzp committed 4 years ago

da201ad4

feat(topology/metric_space): define a pseudo metrizable space (#14053)

urkud committed 4 years ago

600d8eaa

feat(algebra/homology): short exact sequences (#14009)

kim-em committed 4 years ago

e2eea550

feat(data/zmod/quotient): The minimal period equals the cardinality of the orbit (#14183)

tb65536 committed 4 years ago

3d279118

Newer Older