leanprover-community/mathlib

Pull Requests Commits

catching up to mathlib

agusakov committed 4 years ago

0ec961b1

just added begin..end block

agusakov committed 4 years ago

3e514714

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

apnelson1 committed 4 years ago

e34c4672

initial commit (broken)

apnelson1 committed 4 years ago

c00db3ca

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

chore(*): speed up slow proofs (#7253)

sgouezel committed 4 years ago

0dfac6eb

feat(algebra/module/submodule_lattice): add lemmas for nat submodules (#7221)

riccardobrasca committed 4 years ago

829d7733

feat(data/{int, nat}/parity): rename `ne_of_odd_sum` (#7261)

benjamindavidson committed 4 years ago

6f0c4fb3

chore(algebra/group): missed generalizations to mul_one_class (#7259)

eric-wieser committed 4 years ago

fc5e8cb0

fix(equiv/ring): fix bad typeclasses on ring_equiv.trans_apply (#7258)

eric-wieser committed 4 years ago

184e0fe4

feat(linear_algebra/eigenspace): `mem_maximal_generalized_eigenspace` (#7162)

ocfnash committed 4 years ago

77f5fb33

feat(algebra/module/projective): add projective module (#6813)

kbuzzard committed 4 years ago

15a64f53

Older