leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/graded_monoid): switch to heq

eric-wieser committed 3 years ago

cdf9884c

feat(linear_algebra/trace): trace of prod_map (#13872)

antoinelab01 committed 3 years ago

1e011e3f

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

leanprover-community-bot committed 3 years ago

735fbe05

feat(data/polynomial/mirror): `mirror_eq_iff` (#14238)

tb65536 committed 3 years ago

a5878bbe

refactor(category_theory/discrete): make discrete irreducible (#13762)

kim-em committed 3 years ago

c9c9fa15

feat (algebra/group/prod): Showing that embed_product is injective (#14247)

laughinggas committed 3 years ago

5cf7a1c5

feat(algebra/group/conj): instances + misc (#13943)

ericrbg committed 3 years ago

3c6f16c3

chore(*) : `zero_dvd_iff.1` → `eq_zero_of_zero_dvd` (#14241)

vihdzp committed 3 years ago

c8f2a1f4

feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant (#11708)

laughinggas committed 3 years ago

ffe70020

chore(linear_algebra/quadratic_form/basic): remove redundant fields (#14246)

eric-wieser committed 3 years ago

d403cadd

doc(tactic/lint/type_classes): Fix small typo (#14242)

vihdzp committed 3 years ago

218d66a1

feat(group_theory/quotient_group): properties of quotients of homomorphisms and equivalences (#13046)

Multramate committed 3 years ago

e29d9110

feat(order/complete_lattice): add `Sup_diff_singleton_bot` etc (#14205)

urkud committed 3 years ago

18624efa

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

Older