leanprover-community/mathlib

Pull Requests Commits

move files around

adomani committed 3 years ago

000e20b4

adomani committed 3 years ago

49923b8c

add file tactic.congrm

adomani committed 3 years ago

3f55e503

refactor(set_theory/game/*): Fix bad notation `<` on (pre-)games (#13963)

vihdzp committed 3 years ago

b8d8a5e4

feat(linear_algebra/projection) : projections are conjugate to prod_map id 0 (#13802)

antoinelab01 committed 3 years ago

1f00800d

feat(analysis/special_functions/exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579)

astrainfinita committed 3 years ago

e7386121

feat(category_theory): missing comp_ite lemma (#14143)

kim-em committed 3 years ago

570db888

feat(algebra/big_operators): prod_ite_irrel (#14142)

kim-em committed 3 years ago

ad5edeb5

chore(set_theory/ordinal/{basic, arithmetic}): Remove redundant `function` namespace (#14133)

vihdzp committed 3 years ago

05997bda

doc(data/real/sqrt): Fix typo in described theorem (#14126)

timotree3 committed 3 years ago

9d022d77

chore(category_theory/*): move some elementwise lemmas earlier (#13998)

kim-em committed 3 years ago

4125b9ad

feat(set_theory/cardinal/cofinality): Cofinality of `nfp` and `deriv` (#12556)

vihdzp committed 3 years ago

c992b04d

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

Older