leanprover-community/mathlib

Pull Requests Commits

feat(data/complex|matrix): instances of star_ordered_ring and star_ordered_algebra (#4686)

kim-em committed 5 years ago

85636f9a

feat(topology/separation): a cont. function with a cont. left inverse is a closed embedding (#6329)

urkud committed 5 years ago

196c2a8a

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

leanprover-community-bot committed 5 years ago

9bad59cf

fix(data/int/basic,category_theory/equivalence): use neg not minus in lemma names (#6384)

eric-wieser committed 5 years ago

4a391c9d

feat(category_theory/abelian/additive_functor): Adds definition of additive functors (#6367)

adamtopaz committed 5 years ago

358fdf23

chore(data/equiv/local_equiv,topology/local_homeomorph,data/set/function): review (#6306)

urkud committed 5 years ago

b4d2ce45

feat(data/real/sqrt): add continuity attributes (#6388)

benjamindavidson committed 5 years ago

387db0d9

doc(measure_theory/interval_integral): move comment (#6386)

fpvandoorn committed 5 years ago

8cfada11

feat(data/list/basic): nth_drop (#6381)

pechersky committed 5 years ago

2d51a449

chore(group_theory/coset): right_coset additions and module doc (#6371)

Julian-Kuelshammer committed 5 years ago

63e75351

feat(logic/basic): subsingleton_iff_forall_eq (#6379)

kex-y committed 5 years ago

750d117d

feat(algebra/lie/nilpotent): basic facts about nilpotent Lie algebras (#6378)

ocfnash committed 5 years ago

59bf982e

feat(ring_theory/power_series/well_known): sum of power of exponentials (#6368)

mo271 committed 5 years ago

4b22c39d

feat(measure_theory/integration): add theorems about the product of independent random variables (#6106)

mzinkevi committed 5 years ago

e3d6cf82

feat(category_theory/subobject): the semilattice_inf/sup of subobjects (#6278)

kim-em committed 5 years ago

f84f5b2e

feat(chain_complex): lemmas about eq_to_hom (#6250)

kim-em committed 5 years ago

7f46c811

feat(data/buffer/basic): read and to_buffer lemmas (#6048)

pechersky committed 5 years ago

8d3efb71

feat(logic/basic): subsingleton_of_forall_eq (#6376)

kex-y committed 5 years ago

391c90a3

feat(ring_theory/power_series/basic): coeff_succ_X_mul (#6370)

mo271 committed 5 years ago

e6d23d23

feat({group,ring}_theory/free_*): make free_ring.lift and free_comm_ring.lift equivs (#6364)

eric-wieser committed 5 years ago

3ff92489

feat(algebra/regular): lemmas for powers of regular elements (#6356)

adomani committed 5 years ago

b7a7b3d9

fix(data/set/finite): add decidable assumptions (#6264)

kbuzzard committed 5 years ago

ec36fc06

feat(order/well_founded_set): defining `is_partially_well_ordered` to prove `is_wf.add` (#6226)

awainverse committed 5 years ago

680e8eda

lint(set_theory/ordinal): fix def/lemma (#6369)

urkud committed 5 years ago

5931c5cb

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

leanprover-community-bot committed 5 years ago

3c66fd1c

feat(data/fintype/intervals): Add set.finite lemmas for integer intervals (#6365)

Ruben-VandeVelde committed 5 years ago

7a918225

chore(data/equiv/*): add missing coercion lemmas for equivs (#6268)

eric-wieser committed 5 years ago

c0389845

feat(ring_theory/power_series/well_known): power of exponential (#6330)

mo271 committed 5 years ago

283aafff

chore(topology): move `exists_compact_superset`, drop assumption `t2_space` (#6327)

urkud committed 5 years ago

0fb6adae

feat(ring_theory/polynomial/basic): add quotient_equiv_quotient_mv_polynomial (#6287)

riccardobrasca committed 5 years ago

db00ee42

Newer Older