leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/parity): addition/subtraction of even/odd nats (#5934)

benjamindavidson committed 5 years ago

fc7daa36

feat(tactic/norm_fin): tactic for normalizing `fin n` expressions (#5820)

pechersky committed 5 years ago

893ce8b6

refactor(*): rename subtype_congr to subtype_equiv (#6004)

pechersky committed 5 years ago

75a7ce9f

chore(topology/bases): rewrite 2 proofs using tactic mode (#5996)

urkud committed 5 years ago

fec8ee4e

feat(data/finset/basic): add lemmas about bUnion and images of functions on finsets (#5887)

agusakov committed 5 years ago

0c26bb09

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

leanprover-community-bot committed 5 years ago

2c62c0bd

feat(order/compactly_generated, ring_theory/noetherian): the lattice of submodules is compactly generated (#5944)

awainverse committed 5 years ago

a301ef7e

feat(combinatorics/simple_graph/basic): add decidable instance for adjacency of complement (#6000)

agusakov committed 5 years ago

4d3b26f8

feat(data/list/basic) add update_nth_comm (#5989)

alexjbest committed 5 years ago

1706e552

refactor(ring_theory/ideal/*, ring_theory/jacobson): use `comm_semiring` instead of `comm_ring` for ideals (#5954)

adomani committed 5 years ago

9b779f40

chore(group_theory/coset): rename lemmas to follow naming conventions (#5998)

AdrianDoM committed 5 years ago

829c1a50

chore(*): split some long lines (#5997)

urkud committed 5 years ago

684f4f50

fix(archive/imo/*): fixed syntax for docstrings (#5994)

Julian-Kuelshammer committed 5 years ago

acabfa68

fix(topology/algebra/infinite_sum): add missing decidable arguments (#5993)

eric-wieser committed 5 years ago

a84a80d5

feat(list/{zip,indexes}): Add `zip_with` and `map_with_index` lemmas (#5974)

RaitoBezarius committed 5 years ago

64283ce9

chore(*) add mod_add_div' and div_add_mod' and golf proofs (#5962)

Julian-Kuelshammer committed 5 years ago

cbd88d63

chore(linear_algebra/quadratic_form): add two missing simp lemmas about subtraction (#5985)

eric-wieser committed 5 years ago

866e4fda

doc(algebra/category/*): provide two short docstrings and shorten lines (#5984)

Julian-Kuelshammer committed 5 years ago

f2c84aa0

chore(analysis/normed_space/inner_product): add {bilin,sesq}_form_of_inner_apply simp lemmas (#5982)

eric-wieser committed 5 years ago

b1ab3107

feat(data/pnat/basic) pnat can_lift instances (#5977)

alexjbest committed 5 years ago

398e7ad5

feat(category_theory/nat_iso): dsimp lemma for natural isomorphisms (#5973)

b-mehta committed 5 years ago

89c79633

chore(category_theory/monad): generate simp lemmas (#5972)

b-mehta committed 5 years ago

82735883

chore(category_theory/adjunction): reflective lemmas (#5968)

b-mehta committed 5 years ago

3f9b0355

chore(*): split some long lines (#5988)

urkud committed 5 years ago

c5e0d103

chore(*): golf some proofs (#5983)

urkud committed 5 years ago

f060e09c

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

leanprover-community-bot committed 5 years ago

609f5f74

refactor(data/polynomial/degree/definitions): rw -> exact, use term mode proof (#5946)

Jesse Michael Han committed 5 years ago

a15e64af

feat(analysis/analytic/inverse): inverse of a formal multilinear series (#5852)

sgouezel committed 5 years ago

4f4a9b58

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

leanprover-community-bot committed 5 years ago

1ea538b3

chore(algebra/algebra/basic): add simp lemma about `algebra_map ℚ` (#5970)

eric-wieser committed 5 years ago

ae1b5302

Newer Older