leanprover-community/mathlib3

Pull Requests Commits

add suggested documentation

101damnations committed 3 years ago

3ae2284c

make group_algebra a def

101damnations committed 3 years ago

e3abb5ad

remove >100 char lines

101damnations committed 3 years ago

7dc25beb

applying suggestions, expanding docs

101damnations committed 3 years ago

3734fd2e

Merge branch 'group-ring' of https://github.com/leanprover-community/mathlib into group-ring

101damnations committed 3 years ago

6afa736c

remove ext and sl

101damnations committed 3 years ago

6f7a82e9

Merge remote-tracking branch 'origin/master' into group-ring

eric-wieser committed 3 years ago

7ef4114e

feat(group_theory/submonoid/operations): prod_le_iff and le_prod_iff, also for groups and modules (#11898)

nomeata committed 3 years ago

59325814

refactor(number_theory/bernoulli_polynomials): improve names (#11805)

oxarbitrage committed 3 years ago

2b68801b

feat(analysis/complex): a few lemmas about `dist` and `conj` (#11913)

urkud committed 3 years ago

1077eb3c

feat(linear_algebra/basis): `basis.map_equiv_fun` (#11888)

jsm28 committed 3 years ago

36d3b688

style(analysis/special_functions/trigonometric/angle): make types of `sin` and `cos` explicit (#11902)

jsm28 committed 3 years ago

f94b0b31

feat(topology/sheaf_condition): connect sheaves on sites and on spaces without has_products (#11706)

alreadydone committed 3 years ago

9ceb3c2a

chore(data/finsupp/basic): generalize comap_mul_action (#11900)

eric-wieser committed 3 years ago

436966c1

feat(algebra/big_operators/basic): add multiset.prod_sum (#11885)

Ruben-VandeVelde committed 3 years ago

7b91f008

feat(analysis/inner_product_space/basic): `orthonormal.map_linear_isometry_equiv` (#11893)

jsm28 committed 3 years ago

02c9d69d

feat(analysis/complex/isometry): `rotation_symm` (#11891)

jsm28 committed 3 years ago

c61ea33b

feat(analysis/complex/circle): `exp_map_circle_neg` (#11889)

jsm28 committed 3 years ago

2364a091

feat(analysis/special_functions/trigonometric/angle): `sin`, `cos` (#11887)

jsm28 committed 3 years ago

99215e3d

feat(analysis/special_functions/trigonometric/angle): `induction_on` (#11886)

jsm28 committed 3 years ago

98ef84ef

feat(data/list): add some lemmas. (#11879)

Ruben-VandeVelde committed 3 years ago

26179ccd

feat(category_theory/limits): is_limit.exists_unique (#11875)

TwoFX committed 3 years ago

dcbb59c4

feat(category_theory/limits): (co)equalizers in the opposite category (#11874)

TwoFX committed 3 years ago

556483f4

feat(data/set/opposite): the opposite of a set (#11860)

TwoFX committed 3 years ago

7a2a5468

feat(order/complete_lattice): infi_le_iff (#11810)

PatrickMassot committed 3 years ago

0354e56f

chore(algebra/monoid_algebra): generalize lift_nc (#11881)

eric-wieser committed 3 years ago

a2f3f55e

feat(data/pfun): Composition of partial functions (#11865)

YaelDillies committed 3 years ago

04b9d281

chore(model_theory/*): Split up model_theory/basic (#11846)

awainverse committed 3 years ago

00908913

feat(analysis/normed_space/linear_isometry): `symm_trans` (#11892)

jsm28 committed 3 years ago

3c70566a

refactor(data/quot): Make more `setoid` arguments implicit (#11824)

YaelDillies committed 3 years ago

b1b09eb3

Older