leanprover-community/mathlib3

Pull Requests Commits

stated div_mul_inv_singleton

faenuccio committed 5 years ago

ca0f7590

feat(category_theory/limits): Any small complete category is a preorder (#4907)

b-mehta committed 5 years ago

246df99f

feat(category_theory/limits/presheaf): left adjoint if preserves colimits (#4896)

b-mehta committed 5 years ago

40245977

chore(algebra/module/linear_map): Derive linear_map from mul_action_hom (#4888)

eric-wieser committed 5 years ago

6a1ce57b

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

urkud committed 5 years ago

2f07ff21

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

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

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

feat(category_theory/limits/types): explicit description of equalizers in Type (#4880)

b-mehta committed 5 years ago

918e28ca

chore(data/set/intervals/ord_connected): make it more useful as a typeclass (#4879)

urkud committed 5 years ago

34c3668e

feat(*/multilinear): define `(continuous_)multilinear_map.restrict_scalars` (#4872)

urkud committed 5 years ago

9851a886

Older