leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/limits/preserves): transfer preserving limits through nat iso (#4932)

b-mehta committed 5 years ago

9a0ba082

feat(category_theory/limits/shapes/equalizers): equalizer comparison map (#4927)

b-mehta committed 5 years ago

c494db5c

feat(category_theory/limits/preserves): transfer reflecting limits through nat iso (#4934)

b-mehta committed 5 years ago

11368e1b

feat(category_theory/limits/preserves/shapes/products): preserve products (#4857)

b-mehta committed 5 years ago

655b6171

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

leanprover-community-bot committed 5 years ago

c4e8d748

chore(data/polynomial/monic): speedup next_coeff_mul (#4920)

jcommelin committed 5 years ago

8ba0ddef

fix(meta/expr): adjust is_likely_generated_binder_name to lean#490 (#4915)

JLimperg committed 5 years ago

e0cf0d37

feat(category_theory/limits/creates): composition creates limits (#4922)

b-mehta committed 5 years ago

b6b41c10

feat(category_theory/limits/preserves): instances for composition preserving limits (#4921)

b-mehta committed 5 years ago

4f673bde

feat(category_theory/limits): equivalence creates colimits (#4923)

b-mehta committed 5 years ago

bddc5c9e

feat(src/ring_theory/polynomial/cyclotomic): cyclotomic polynomials (#4914)

riccardobrasca committed 5 years ago

91f8e687

chore(algebra/lie/basic): Add some missing simp lemmas about A →ₗ⁅R⁆ B (#4912)

eric-wieser committed 5 years ago

747aaae9

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

leanprover-community-bot committed 5 years ago

fd3212c3

feat(ring_theory): define a `power_basis` structure (#4905)

Vierkantor committed 5 years ago

a12d6772

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

Newer Older