leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 4 years ago

5d206164

Merge remote-tracking branch 'origin/master' into eric-wieser/direct_sum-monoid_algebra

eric-wieser committed 4 years ago

d5d1ebf3

eric-wieser committed 4 years ago

5e206bfb

replace a duplicate definition

eric-wieser committed 4 years ago

fca73809

replace a duplicate definition

eric-wieser committed 4 years ago

c4536aa9

feat(data/finsupp/to_dfinsupp): add equivalences between finsupp and dfinsupp

eric-wieser committed 4 years ago

7748d2d1

eric-wieser committed 4 years ago

3d5893ea

Add another missing decidable argument

eric-wieser committed 4 years ago

5049619a

Add another missing decidable argument

eric-wieser committed 4 years ago

a03bd0ab

eric-wieser committed 4 years ago

af1e5ffe

fix(data/finsupp/basic): add a missing decidable argument

eric-wieser committed 4 years ago

Verified 0b9e6403

doc(data/quot): promote a comment to a docstring (#7306)

eric-wieser committed 4 years ago

f08fe5fd

feat(data/dfinsupp): copy map_range defs from finsupp (#7293)

eric-wieser committed 4 years ago

7db1181e

feat(data/finset/lattice): add `comp_sup'_eq_sup'_comp`, golf some proofs (#7275)

eric-wieser committed 4 years ago

80028f3a

feat(category_theory/monoidal): Drinfeld center (#7186)

kim-em committed 4 years ago

9b8d6e49

refactor(order/well_founded_set): partially well ordered sets using relations other than `has_le.le` (#7131)

awainverse committed 4 years ago

923314f2

feat(group_theory/{order_of_element, perm/cycles}): two cycles are conjugate iff their supports have the same size (#7024)

awainverse committed 4 years ago

02a31338

feat(algebra/algebra/basic): add alg_hom.apply (#7278)

eric-wieser committed 4 years ago

8481bf46

feat(algebra/big_operators): product over coerced fintype (#7236)

b-mehta committed 4 years ago

4abf9618

refactor(group_theory/submonoid): adjust definitional unfolding of add_monoid_hom.mrange to match set.range (#7227)

eric-wieser committed 4 years ago

ad588611

feat(algebraic_geometry/prime_spectrum): More lemmas (#7244)

justus-springer committed 4 years ago

9bdc5551

feat(logic/basic): exists_or_eq_{left,right} (#7224)

pechersky committed 4 years ago

39d23b8e

feat(linear_algebra/bilinear_form): Unique adjoints with respect to a nondegenerate bilinear form (#7071)

kex-y committed 4 years ago

bf22ab3f

feat(category_theory/subobject): easy facts about the top subobject (#7267)

TwoFX committed 4 years ago

a4f59bde

feat(algebra/lie/abelian): expand API for `lie_module.maximal_trivial_submodule` (#7235)

ocfnash committed 4 years ago

0c721d5d

chore(combinatorics/quiver): make quiver a class (#7150)

kim-em committed 4 years ago

944ffff9

feat(category_theory/abelian): definition of projective object (#7108)

kim-em committed 4 years ago

5e188d2f

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

leanprover-community-bot committed 4 years ago

013a84eb

chore(data/list): drop `list.is_nil` (#7269)

urkud committed 4 years ago

8bf9fd58

chore(algebra/*): add back nat_algebra_subsingleton and add_comm_monoid.nat_semimodule.subsingleton (#7263)

eric-wieser committed 4 years ago

3ad4dabf

Older