leanprover-community/mathlib

Pull Requests Commits

chore(ring/basic): Remove unnecessary field that can be inherited

eric-wieser committed 5 years ago

Verified c626a475

feat(category_theory/monad): algebras for the coproduct monad (#5679)

b-mehta committed 5 years ago

0c57d1e7

feat(char_p/quotient): Add a lemma to inherit char_p from the underlying ring (#5809)

eric-wieser committed 5 years ago

e41b917c

feat(ring_theory/ideal/operations): generalize quotient of algebras (#5802)

riccardobrasca committed 5 years ago

385173df

feat(category_theory/limits): preserve monomorphisms (#5801)

b-mehta committed 5 years ago

31fd5b58

feat(algebra/lie/basic): additional lemmas concerning `lie_algebra.derived_series_of_ideal` (#5815)

ocfnash committed 5 years ago

a3ef65da

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

leanprover-community-bot committed 5 years ago

b1d56736

chore(algebra/group/hom): Add `mk_coe` lemmas (#5812)

eric-wieser committed 5 years ago

d7a8709e

feat(measure_theory/lp_space): extend the definition of Lp seminorm to p ennreal (#5808)

RemyDegenne committed 5 years ago

b1214293

chore(order/filter/basic): add `eventually_eq.rfl` and `eventually_le.rfl` (#5805)

urkud committed 5 years ago

9d14a5f3

feat(analysis/normed_space,topology/metric_space): distance between diagonal vectors (#5803)

urkud committed 5 years ago

21b0b012

feat(data/buffer/parser/numeral): numeral parser defs (#5462)

pechersky committed 5 years ago

da6e3c36

chore(category_theory/adjunction): move reflective functor lemmas (#5800)

b-mehta committed 5 years ago

8b47563e

feat(algebra/lie/basic): generalise the definition of `lie_algebra.derived_series` (#5794)

ocfnash committed 5 years ago

90763c46

feat(data/list/basic): nth and nth_le for pmap (#5451)

pechersky committed 5 years ago

18841a9e

feat(data/option/basic): map_bind and join_pmap lemmas (#5445)

pechersky committed 5 years ago

9777d1e7

chore(data/matrix/notation): Add some missing simp lemmas for sub, head, and tail (#5807)

eric-wieser committed 5 years ago

c37c64fb

chore(analysis/normed_space): golf some proofs (#5804)

urkud committed 5 years ago

190dd106

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

leanprover-community-bot committed 5 years ago

c9c3b6f5

feat(combinatorics/simple_graph/basic): add lemmas about cardinality of common neighbor set (#5789)

agusakov committed 5 years ago

541688b5

refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774)

jcommelin committed 5 years ago

77003ce2

doc(tactic/rewrite): Add an example for assoc_rw (#5799)

eric-wieser committed 5 years ago

725efb18

refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp` (#5796)

Jesse Michael Han committed 5 years ago

b5e832e2

feat(order/limsup_liminf, order/filter/ennreal): add properties of limsup for ennreal-valued functions (#5746)

RemyDegenne committed 5 years ago

57bc1dab

feat(algebra/lie/basic): results relating Lie algebra morphisms and ideal operations (#5778)

ocfnash committed 5 years ago

66e955e4

doc(data/buffer/parser/basic): fix typo (#5792)

sorawee committed 5 years ago

9381e37d

chore(field_theory/minpoly): meaningful variable names (#5773)

jcommelin committed 5 years ago

8ab1a39d

feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703)

riccardobrasca committed 5 years ago

db617b3c

chore(category_theory/monad): golf and lint monadic adjunctions (#5769)

b-mehta committed 5 years ago

f3d3d046

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

leanprover-community-bot committed 5 years ago

3089b161

Older