leanprover-community/mathlib

Pull Requests Commits

feat(analysis/normed_space/pi_Lp): add missing nnnorm lemmas (#14221)

eric-wieser committed 3 years ago

6906b6f7

docs(category_theory/*): the last missing module docs (#14237)

kim-em committed 3 years ago

ea3009f6

chore(scripts): update nolints.txt (#14239)

leanprover-community-bot committed 3 years ago

923a14da

refactor(set_theory/game/pgame): Rename `le_def_lf` → `le_iff_forall_lf` (#14206)

vihdzp committed 3 years ago

83285b24

feat(topology/algebra/module/basic): add `continuous_linear_map.apply_module` (#14223)

eric-wieser committed 3 years ago

cc74bcbd

feat(category_theory/limits): (co/bi)products over types with a unique term (#14191)

kim-em committed 3 years ago

76f9f454

doc(deprecated/*): all deprecated files now lint (#14233)

kbuzzard committed 3 years ago

c42cff11

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

eric-wieser committed 3 years ago

a5f4cf53

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

vihdzp committed 3 years ago

32700f50

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

antoinelab01 committed 3 years ago

5fe43a91

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

kbuzzard committed 3 years ago

259c951d

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

urkud committed 3 years ago

4f31117e

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

eric-wieser committed 3 years ago

470ddbdb

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

YaelDillies committed 3 years ago

503970d2

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

YaelDillies committed 3 years ago

c38ab356

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

pbazin committed 3 years ago

cfedf1d5

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

MantasBaksys committed 3 years ago

2c2d515a

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

ADedecker committed 3 years ago

54773fc0

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

YaelDillies committed 3 years ago

9dc9c3ea

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

eric-wieser committed 3 years ago

ae6a7c3f

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

vihdzp committed 3 years ago

59facea4

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

urkud committed 3 years ago

d08f7340

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

vihdzp committed 3 years ago

50696a85

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

tb65536 committed 3 years ago

9f6f605b

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

kim-em committed 3 years ago

f48cbb16

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

vihdzp committed 3 years ago

ca5930df

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

urkud committed 3 years ago

6b291d7b

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

mans0954 committed 3 years ago

632fef37

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

YaelDillies committed 3 years ago

0afb90b4

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

aronerben committed 3 years ago

21581937

Newer Older