leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/kernels): helper lemmas for constructing kernels (#3439)

kim-em committed 6 years ago

31699708

refactor(linear_algebra/*): postpone importing material on direct sums (#3484)

kim-em committed 6 years ago

d174d3d0

feat(ring_theory/jacobson): definition of Jacobson rings (#3404)

dtumad committed 6 years ago

c71e67a9

refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481)

Nicknamen committed 6 years ago

0322d892

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

leanprover-community-bot committed 6 years ago

079d4093

refactor(ring_theory): remove unbundled leftovers in `ideal.quotient` (#3467)

Vierkantor committed 6 years ago

6721ddfb

feat(category_theory/kernels): cokernel (image.ι f) ≅ cokernel f (#3441)

kim-em committed 6 years ago

564ab022

fix(tactic/library_search): group monotone lemmas with le lemmas (#3471)

kim-em committed 6 years ago

32c082f5

feat(data/finset/basic): Cardinality of intersection with singleton (#3480)

Smaug123 committed 6 years ago

2915faed

feat(topology/local_extr): add lemmas on composition with continuous functions (#3459)

dupuisf committed 6 years ago

1f74ddd2

fix(algebra/group/units): add missing coe lemmas to units (#3472)

alexpeattie committed 6 years ago

7aa85c2b

feat(data/multivariate/qpf): definition (#3395)

cipher1024 committed 6 years ago

b66d1bee

feat(tactic/squeeze_*): improve suggestions (#3431)

cipher1024 committed 6 years ago

78f438b7

feat(data/equiv/mul_add): refl_apply and trans_apply (#3470)

ChrisHughes24 committed 6 years ago

d0df6b81

feat(solve_by_elim): add tracing (#3468)

kim-em committed 6 years ago

2994f1b9

feat(set_theory/cardinal): simp lemmas about numerals (#3450)

kim-em committed 6 years ago

38b95c8a

feat(logic/basic): nonempty.some (#3449)

kim-em committed 6 years ago

9a923639

refactor(tactic/generalizes): reimplement generalizes' (#3416)

JLimperg committed 6 years ago

469043f9

feat(linear_algebra/affine_space): lemmas on affine spans (#3453)

jsm28 committed 6 years ago

593b1bb5

refactor(data/polynomial/*): further refactors (#3435)

kim-em committed 6 years ago

65208ed7

feat(tactic/interactive_expr): always select all arguments (#3384)

gebner committed 6 years ago

cb062145

chore(algebra/ring): fix a mistake (#3469)

jcommelin committed 6 years ago

4a3755a1

feat (algebra/module): lemma about submodules (#3466)

smorel394 committed 6 years ago

4dc0814e

fix(tactic/library_search): 1 ≤ n goals in nat (#3462)

kim-em committed 6 years ago

a400adb9

feat(data/padics/padic_norm): lemmas about padic_val_nat (#3230)

Smaug123 committed 6 years ago

5080dd56

feat(data/nat/digits): a bigger number has more digits (#3457)

SnobbyDragon committed 6 years ago

84d4ea77

feat(field_theory/tower): tower law (#3355)

kckennylau committed 6 years ago

792f5415

feat(data/quot.lean): add lift_on_beta\_2 (#3456)

stanescuUW committed 6 years ago

501aeb7f

feat(tactic/unfold_cases): add unfold_cases tactic (#3396)

DanielFabian committed 6 years ago

697488c8

chore(tactic/interactive): move non-monadic part of `clean` to `expr.clean` (#3461)

urkud committed 6 years ago

2975f93a

Newer Older