leanprover-community/mathlib3

Pull Requests Commits

feat(*): Add surjective -> surjection

eric-wieser committed 5 years ago

7cfbe063

feat(data/equiv/one_sided): Add bundled one-sided inverses

eric-wieser committed 5 years ago

257eefa8

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

leanprover-community-bot committed 5 years ago

a19e48b1

feat(data/nat/modeq): Generalised version of the Chinese remainder theorem (#5683)

alexjbest committed 5 years ago

b2d95c0c

feat(field_theory/normal): Splitting field is normal (#5768)

tb65536 committed 5 years ago

8b6f541e

chore(data/list/range): Add range_zero and rename range_concat to range_succ (#5821)

eric-wieser committed 5 years ago

7c892653

chore(data/dfinsupp): add `dfinsupp.prod_comm` (#5817)

eric-wieser committed 5 years ago

2ec396a7

refactor(data/fin): shorter proof of `mk.inj_iff` (#5811)

Jesse Michael Han committed 5 years ago

9cdffe9c

feat(data/list/range): nth_le_fin_range (#5456)

pechersky committed 5 years ago

c700791b

feat(data/fin): add_comm_monoid and simp lemmas (#5010)

pechersky committed 5 years ago

9ae33174

feat(algebraic_geometry/is_open_comap_C): add file is_open_comap_C, prove that Spec R[x] \to Spec R is an open map (#5693)

adomani committed 5 years ago

a7a4f34c

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

Older