leanprover-community/mathlib3

Pull Requests Commits

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

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

urkud committed 4 years ago

120feb11

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

ocfnash committed 4 years ago

26e6d4cb

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

urkud committed 4 years ago

78eb83a3

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

eric-wieser committed 4 years ago

aa730c63

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

eric-wieser committed 4 years ago

ffb6a582

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

adomani committed 4 years ago

9d54837a

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

b-mehta committed 4 years ago

87a021cd

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

eric-wieser committed 4 years ago

69b93fcb

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

tb65536 committed 4 years ago

0e519766

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

pechersky committed 4 years ago

a3d951bc

feat(algebraic_geometry/prime_spectrum): specialization order (#6286)

jcommelin committed 4 years ago

2b6dec0b

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

leanprover-community-bot committed 4 years ago

dc781774

feat(algebra/group_power/basic): `abs_lt_abs_of_sqr_lt_sqr` (#6277)

benjamindavidson committed 4 years ago

2134d0c1

feat(data/list/basic): repeat injectivity (#6337)

pechersky committed 4 years ago

b8b87559

feat(data/dfinsupp): add coe lemmas (#6343)

eric-wieser committed 4 years ago

87f8db2e

docs(undergrad.yaml): recent changes (#6313)

hrmacbeth committed 4 years ago

96ae2ad1

chore(topology/order): drop an unneeded argument (#6345)

urkud committed 4 years ago

4355d171

feat(data/list/basic): drop_eq_nil_iff_le (#6336)

pechersky committed 4 years ago

ab03ebe7

feat(topology/locally_constant): basics on locally constant functions (#6192)

jcommelin committed 4 years ago

473bb7d4

feat(measure_theory/interval_integral): add simp attribute to `integral_const` (#6334)

benjamindavidson committed 4 years ago

f470cc62

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

leanprover-community-bot committed 4 years ago

4d4c7bb9

chore(topology/bases): golf a proof (#6326)

urkud committed 4 years ago

93d17601

refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs (#6311)

eric-wieser committed 4 years ago

08ea23b2

fix(algebra/group/pi): remove unnecessary add_monoid requirement from pi.single_zero (#6325)

eric-wieser committed 4 years ago

dccc5421

Newer Older