leanprover-community/mathlib

Pull Requests Commits

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

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

Vierkantor committed 5 years ago

cc9d3ab1

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

robertylewis committed 5 years ago

7abfbc92

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

laughinggas committed 5 years ago

70d71149

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

Julian-Kuelshammer committed 5 years ago

4daac664

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

laughinggas committed 5 years ago

6d2726c6

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

laughinggas committed 5 years ago

46fb0d8b

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

Julian-Kuelshammer committed 5 years ago

12bb9aee

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

Julian-Kuelshammer committed 5 years ago

a10c19d0

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

urkud committed 5 years ago

590442ad

refactor(order/filter,topology): review API (#6347)

urkud committed 5 years ago

120feb11

feat(algebra/lie/{subalgebra,submodule}): grab bag of new lemmas (#6342)

ocfnash committed 5 years ago

26e6d4cb

feat(linear_algebra/pi): add `pi.lsum` (#6335)

urkud committed 5 years ago

78eb83a3

feat(linear_algebra): a module has a unique submodule iff it has a unique element (#6281)

eric-wieser committed 5 years ago

aa730c63

feat(data/sigma/basic): add a more convenient ext lemma for equality of sigma types over subtypes (#6257)

eric-wieser committed 5 years ago

ffb6a582

feat(data/polynomial/degree): lemmas on nat_degree and behaviour under multiplication by constants (#6224)

adomani committed 5 years ago

9d54837a

feat(data/quot): `quotient.rec_on_subsingleton` with implicit setoid (#6346)

b-mehta committed 5 years ago

87a021cd

fix(data/finsupp/basic): delta-reduce the definition of coe_fn_injective (#6344)

eric-wieser committed 5 years ago

69b93fcb

feat(data/polynomial/reverse): Trailing degree is multiplicative (#6351)

tb65536 committed 5 years ago

0e519766

feat(data/nat/digits): digits injective at fixed base (#6338)

pechersky committed 5 years ago

a3d951bc

Newer Older