leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/concrete_category): id_apply, comp_apply (#7530)

jcommelin committed 5 years ago

f44a5eb1

feat(ring_theory/localization): Characterize units in localization at prime ideal (#7519)

justus-springer committed 5 years ago

0ead8ee9

feat(data/list/basic): non-meta to_chunks (#7517)

digama0 committed 5 years ago

755cb75f

feat(linear_algebra/tensor_product): distrib_mul_actions are inherited (#7516)

eric-wieser committed 5 years ago

930485c1

chore(algebra/module/linear_map): add missing rfl lemmas (#7515)

eric-wieser committed 5 years ago

b903ea28

feat(category_theory/opposites): Adds equivalences for functor categories. (#7505)

adamtopaz committed 5 years ago

6d25f3ae

feat(data/dfinsupp): add `finset_sum_apply` and `coe_finset_sum` (#7499)

eric-wieser committed 5 years ago

efb283ca

feat(normed_space/normed_group_hom): add lemmas (#7468)

riccardobrasca committed 5 years ago

9acbe588

feat(category_theory/subobjects): more about kernel and image subobjects (#7467)

kim-em committed 5 years ago

154fda29

feat(data/real/basic): add real.Inf_le_iff (#7524)

riccardobrasca committed 5 years ago

bb1fb897

feat(data/polynomial/*): Specific root sets (#7510)

tb65536 committed 5 years ago

e00d6e08

chore(data/equiv/basic): Show that `Pi_curry` is really just `sigma.curry` (#7497)

eric-wieser committed 5 years ago

6f27ef7c

feat(data/finsupp,linear_algebra): `finsupp.split` is an equivalence (#7490)

Vierkantor committed 5 years ago

9aed6c94

feat(data/equiv,linear_algebra): `Pi_congr_right` for `mul_equiv` and `linear_equiv` (#7489)

Vierkantor committed 5 years ago

48bdd1e3

feat(data/nat/choose/sum): alternate forms of the binomial theorem (#7415)

ocfnash committed 5 years ago

652357ac

refactor(ring_theory/ideal/operations.lean): make is_prime.comap an instance (#7518)

justus-springer committed 5 years ago

9c86e381

feat(category_theory/linear): linear functors (#7369)

kim-em committed 5 years ago

13c41e1f

feat(category_theory): the opposite of an abelian category is abelian (#7514)

kim-em committed 5 years ago

7040c50c

feat(linear_algebra/finsupp): linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M` (#7472)

Vierkantor committed 5 years ago

c4c6cd81

feat(algebra/*, ring_theory/valuation/basic): `linear_ordered_add_comm_group_with_top`, `add_valuation.map_sub` (#7452)

awainverse committed 5 years ago

9154a830

feat(category_theory/.../zero): if a zero morphism is a mono, the source is zero (#7462)

kim-em committed 5 years ago

6af5fbd2

feat(measure_theory/set_integral): continuous_on.measurable_at_filter (#7511)

benjamindavidson committed 5 years ago

009be861

feat(category_theory/Fintype): some lemmas and `Fintype_to_Profinite`. (#7491)

adamtopaz committed 5 years ago

709c73b2

feat(data/finsupp): prove `f.curry x y = f (x, y)` (#7475)

Vierkantor committed 5 years ago

1ef04bde

feat(algebra/big_operators): telescopic sums (#7470)

PatrickMassot committed 5 years ago

d3a46a7f

feat(order/filter_at_top_bot): extraction lemmas (#7469)

PatrickMassot committed 5 years ago

18ada66c

feat(category_theory/subobject): minor tweaks (#7466)

kim-em committed 5 years ago

7cc367b7

feat(category_theory/quotient): the quotient functor is full and essentially surjective (#7465)

kim-em committed 5 years ago

e25cbe0d

feat(category_theory/preadditive): reformulation of mono_of_kernel_zero (#7464)

kim-em committed 5 years ago

19b752c4

feat(category_theory/.../additive_functor): additive functors preserve zero objects (#7463)

kim-em committed 5 years ago

77949694

Newer Older