leanprover-community/mathlib

Pull Requests Commits

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

AdrianDoM committed 4 years ago

829c1a50

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

urkud committed 4 years ago

684f4f50

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

Julian-Kuelshammer committed 4 years ago

acabfa68

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

eric-wieser committed 4 years ago

a84a80d5

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

RaitoBezarius committed 4 years ago

64283ce9

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

Julian-Kuelshammer committed 4 years ago

cbd88d63

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

eric-wieser committed 4 years ago

866e4fda

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

Julian-Kuelshammer committed 4 years ago

f2c84aa0

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

eric-wieser committed 4 years ago

b1ab3107

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

alexjbest committed 4 years ago

398e7ad5

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

b-mehta committed 4 years ago

89c79633

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

b-mehta committed 4 years ago

82735883

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

b-mehta committed 4 years ago

3f9b0355

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

urkud committed 4 years ago

c5e0d103

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

urkud committed 4 years ago

f060e09c

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

leanprover-community-bot committed 4 years ago

609f5f74

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

Jesse Michael Han committed 4 years ago

a15e64af

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

sgouezel committed 4 years ago

4f4a9b58

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

leanprover-community-bot committed 4 years ago

1ea538b3

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

eric-wieser committed 4 years ago

ae1b5302

feat(geometry/manifold/instances): sphere is a topological manifold (#5591)

hrmacbeth committed 4 years ago

f596077f

feat(field_theory/normal): Restriction is surjective (#5960)

tb65536 committed 4 years ago

a6c0442b

feat(algebra/lie/basic): define derived length and semisimple Lie algebras (#5930)

ocfnash committed 4 years ago

48d05924

feat(topology/instances/nnreal): add has_sum_nat_add_iff and module docstring (#5716)

kbuzzard committed 4 years ago

539550d0

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

urkud committed 4 years ago

d6fe605f

feat(measure_theory): Absolute continuity (#5948)

fpvandoorn committed 4 years ago

8069521e

doc(group_theory/order_of_element): Adding doc string (#5936)

Julian-Kuelshammer committed 4 years ago

cf218639

feat(topology/category): compact hausdorff spaces are reflective in Top (#5955)

b-mehta committed 4 years ago

cbcbaa06

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

leanprover-community-bot committed 4 years ago

b44e9dd8

chore(*): fix some "line too long" lint errors by rewriting proofs/statements (#5958)

urkud committed 4 years ago

686d005a

Newer Older