leanprover-community/mathlib3

Pull Requests Commits

vihdzp committed 3 years ago

3d5391c0

Merge branch 'add_left_moves' into add_lf_of_lf_of_lt

vihdzp committed 3 years ago

67ff5461

Merge branch 'master' into add_left_moves

vihdzp committed 3 years ago

3916c185

Merge branch 'add_left_moves' into add_lf_of_lf_of_lt

vihdzp committed 3 years ago

b8901cac

Merge branch 'master' into add_lf_of_lf_of_lt

vihdzp committed 3 years ago

f612d472

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

vihdzp committed 3 years ago

3c0c2e98

Remove `equiv_rw`

vihdzp committed 3 years ago

bf567669

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

Merge branch 'master' into add_left_moves

vihdzp committed 3 years ago

c984daa2

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

Older