leanprover-community/mathlib

Pull Requests Commits

kim-em committed 4 years ago

9eb42eba

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

kex-y committed 4 years ago

750d117d

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

ocfnash committed 4 years ago

59bf982e

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

mo271 committed 4 years ago

4b22c39d

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

mzinkevi committed 4 years ago

e3d6cf82

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

kim-em committed 4 years ago

f84f5b2e

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

kim-em committed 4 years ago

7f46c811

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

pechersky committed 4 years ago

8d3efb71

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

kex-y committed 4 years ago

391c90a3

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

mo271 committed 4 years ago

e6d23d23

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

eric-wieser committed 4 years ago

3ff92489

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

adomani committed 4 years ago

b7a7b3d9

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

kbuzzard committed 4 years ago

ec36fc06

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

awainverse committed 4 years ago

680e8eda

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

urkud committed 4 years ago

5931c5cb

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

leanprover-community-bot committed 4 years ago

3c66fd1c

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

Ruben-VandeVelde committed 4 years ago

7a918225

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

eric-wieser committed 4 years ago

c0389845

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

mo271 committed 4 years ago

283aafff

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

urkud committed 4 years ago

0fb6adae

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

riccardobrasca committed 4 years ago

db00ee42

feat(algebra/module,linear_algebra): generalize `smul_eq_zero` (#6199)

Vierkantor committed 4 years ago

cc9d3ab1

doc(references.bib): add witt vector references and normalize (#6366)

robertylewis committed 4 years ago

7abfbc92

feat(nat/choose): lemmas regarding binomial coefficients (#6362)

laughinggas committed 4 years ago

70d71149

chore(field_theory/mv_polynomial): generalised to comm_ring and module doc (#6341)

Julian-Kuelshammer committed 4 years ago

4daac664

feat(number_theory/bernoulli): definition and properties of Bernoulli numbers (#6363)

laughinggas committed 4 years ago

6d2726c6

feat(big_operators/intervals): lemma on dependent double sum (#6361)

laughinggas committed 4 years ago

46fb0d8b

chore(linear_algebra/*): split lines and doc `direct_sum/tensor_product` (#6360)

Julian-Kuelshammer committed 4 years ago

12bb9aee

doc(group_theory/*): module docs for `quotient_group` and `presented_group` (#6358)

Julian-Kuelshammer committed 4 years ago

a10c19d0

feat(topology/subset_properties): locally finite family on a compact space is finite (#6352)

urkud committed 4 years ago

590442ad

Older