leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/specific_limits/floor_pow): auxiliary results on series involving floors of powers (#13850)

sgouezel committed 3 years ago

6d4c2027

chore(algebra/invertible): minor golf (#14141)

vihdzp committed 3 years ago

ba9d551a

feat(linear_algebra/matrix/to_lin): equivalence via right multiplication (#13870)

kim-em committed 3 years ago

79bc06bf

chore(*): use notation instead of `set.*` (#14139)

urkud committed 3 years ago

21a71de1

refactor(group_theory/free_abelian_group): Make proofs more robust (#14089)

YaelDillies committed 3 years ago

38244939

feat(.github/workflows): restore merge_conflicts action, running on cron (#14137)

kim-em committed 3 years ago

9f5b3280

feat(data/polynomial/degree/definitions): two more `nat_degree_le` lemmas (#14098)

adomani committed 3 years ago

b7e20ca0

feat(data/nat/totient): add `totient_div_of_dvd` and golf `sum_totient` (#14007)

stuart-presnell committed 3 years ago

6b7fa7ab

feat(archive/imo/imo1975_q1): Add the formalization of IMO 1975 Q1 (#13047)

MantasBaksys committed 3 years ago

55cd1047

feat(data/zmod/quotient): Multiplicative version of `zmultiples_quotient_stabilizer_equiv` (#13948)

tb65536 committed 3 years ago

caa1352a

feat(representation_theory): fdRep k G, the category of finite dim representations of G (#13740)

kim-em committed 3 years ago

03da6818

feat(topology/uniform_space): lemmas about `s ○ s ○ ... ○ s ⊆ t` (#14051)

urkud committed 3 years ago

6a48b384

feat(data/list/{count,perm},data/multiset/basic): countp and count lemmas (#14108)

kmill committed 3 years ago

3185c251

chore(data/real/ennreal): tidy some proofs (#14101)

Ruben-VandeVelde committed 3 years ago

23a22058

feat(set_theory/ordinal/basic): Order isomorphism between `o.out.α` and `set.Iio o` (#14074)

vihdzp committed 3 years ago

7b7af48b

feat(topology/uniform_space/separation): add `filter.has_basis.mem_separation_rel` (#14050)

urkud committed 3 years ago

26f41120

feat(number_theory/von_mangoldt): simple bounds on von mangoldt function (#14033)

b-mehta committed 3 years ago

a2e671bb

feat(set_theory/cardinal/cofinality): Move fundamental sequence results to namespace (#14020)

vihdzp committed 3 years ago

644cae5e

feat(order/filter/lift): drop an unneeded assumption (#14117)

urkud committed 3 years ago

c53285a8

chore(algebra/order/field): fill in TODO for inv anti lemmas (#14112)

b-mehta committed 3 years ago

85124aff

chore(algebra/order/field): fill in missing lemma (#14111)

b-mehta committed 3 years ago

462b9509

feat(data/polynomial/degree/lemmas): two lemmas about `nat_degree`s of sums (#14100)

adomani committed 3 years ago

f6178629

feat(topology/basic): add lemmas like `closure s \ interior s = frontier s` (#14086)

urkud committed 3 years ago

de418aad

feat(data/set/prod): add `prod_self_{s,}subset_prod_self` (#14084)

urkud committed 3 years ago

15f6b527

feat(topology/basic): add `nhds_basis_closeds` (#14083)

urkud committed 3 years ago

14749964

feat(topology/order): add `nhds_true` and `nhds_false` (#14082)

urkud committed 3 years ago

bb97a64b

perf(field_theory/primitive_element): declare auxiliary function `noncomputable!` (#14071)

Vierkantor committed 3 years ago

bd5914f6

feat(data/real/nnreal): add `nnreal.le_infi_add_infi` and other lemmas (#14048)

urkud committed 3 years ago

c4c279e6

feat(linear_algebra/tensor_product): tensor_product.map is bilinear in its two arguments (#13608)

antoinelab01 committed 3 years ago

a945b187

feat(algebra/big_operators/basic): add `sum_erase_lt_of_pos` (#14066)

stuart-presnell committed 3 years ago

17102ae8

Newer Older