leanprover-community/mathlib

Pull Requests Commits

chore(topology/metric_space): more `norm_cast` lemmas, golf proofs (#4911)

urkud committed 5 years ago

2f07ff21

urkud committed 5 years ago

e579b7e9

Merge branch 'master' into box-subadditive

urkud committed 5 years ago

77d7b262

Add missing file

urkud committed 5 years ago

8463b158

urkud committed 5 years ago

a165e5a4

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

leanprover-community-bot committed 5 years ago

834d491d

chore(data/W): rename `W` to `W_type` (#4909)

robertylewis committed 5 years ago

189063b1

feat(ring_theory/witt_vector/teichmuller): Teichmuller representatives (#4690)

jcommelin committed 5 years ago

5a61ef19

feat(logic/basic): forall2_congr lemmas (#4904)

b-mehta committed 5 years ago

211b0c05

feat(ring_theory/algebraic): if `L / K` is algebraic, then the subalgebras are fields (#4903)

Vierkantor committed 5 years ago

0081a5a4

feat(linear_algebra/tensor_product): tensoring linear maps with modules (#4771)

jcommelin committed 5 years ago

e303a7d9

chore(data/finset): add a few lemmas (#4901)

urkud committed 5 years ago

6f72c228

chore(analysis/calculus/times_cont_diff): a few missing lemmas (#4900)

urkud committed 5 years ago

08770779

feat(analysis/calculus/times_cont_diff): add `restrict_scalars` (#4899)

urkud committed 5 years ago

beb6831f

feat(category_theory/limits/cones): map_cone and postcompose lemmas (#4894)

b-mehta committed 5 years ago

b7991c0a

feat(category_theory/closed/cartesian): product preserves colimits (#4893)

b-mehta committed 5 years ago

7d6f37dc

feat(data/equiv): exists unique congr (#4890)

b-mehta committed 5 years ago

e1d60fda

feat(order/filter/at_top_bot): lemmas about `map/comap` of `at_top`/`at_bot` (#4878)

urkud committed 5 years ago

d88042c1

feat(data/quaternion): define quaternions and prove some basic properties (#2339)

urkud committed 5 years ago

7ab3ca85

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

leanprover-community-bot committed 5 years ago

16e38718

Merge branch 'master' into cauchy-rect

urkud committed 5 years ago

c4b1a2bf

feat(category_theory/yoneda): type level yoneda equivalence (#4889)

b-mehta committed 5 years ago

23a2767d

feat(order): countable categoricity of dense linear orders (#2860)

dwarn committed 5 years ago

505097f4

chore(algebra/lie): adjoint rep of lie algebra uses lowercase `ad` (#4891)

jcommelin committed 5 years ago

712a0b75

urkud committed 5 years ago

f4d7f93c

feat(*): assorted prereqs for cyclotomic polynomials (#4887)

riccardobrasca committed 5 years ago

e88a5bb5

feat(category_theory/limits/types): ext iff lemma (#4883)

b-mehta committed 5 years ago

b37d4a3d

fix(tactic/interactive): issue where long term tooltips break layout (#4882)

EdAyers committed 5 years ago

6bed7d4f

feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863)

bryangingechen committed 5 years ago

4f8c490f

urkud committed 5 years ago

61752beb

Newer Older