leanprover-community/mathlib3

Pull Requests Commits

some tests on restricting scalar operations on manifolds

fpvandoorn committed 2 years ago

dae47b6f

feat(geometry/manifold): lemmas from the sphere eversion project (#18877)

fpvandoorn committed 2 years ago

e354e865

chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure (#19160)

RemyDegenne committed 2 years ago

3b92d54a

refactor(geometry/manifold/cont_mdiff_map): refactor to reduce imports (#19164)

kim-em committed 2 years ago

0dc40792

feat (number_theory/zeta_function): func eqn + link to Bernoulli nos (#19158)

loefflerd committed 2 years ago

81843c08

chore(linear_algebra/eigenspace): split file (#19163)

kim-em committed 2 years ago

6b016921

chore(*): add mathlib4 synchronization comments (#19162)

github-actions[bot] committed 2 years ago

c2092722

chore(algebra/algebra/spectrum): split file (#19161)

j-loreaux committed 2 years ago

58a27226

chore(*): add mathlib4 synchronization comments (#19159)

github-actions[bot] committed 2 years ago

36938f77

feat (special_functions/gamma): doubling formula (#19136)

loefflerd committed 2 years ago

a3209ddf

chore(*): add mathlib4 synchronization comments (#19157)

github-actions[bot] committed 2 years ago

575b4ea3

feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n` (#15681)

ralvrz committed 2 years ago

4c3e1721

chore(field_theory/splitting_field): split file (#19154)

riccardobrasca committed 2 years ago

df76f433

chore(archive/imo): fix some naming inconsistencies and whitespace (#19155)

adomani committed 2 years ago

30882647

chore(algebraic_geometry/open_immersion): split (#19149)

hrmacbeth committed 2 years ago

533f62f4

chore(topology/sheaves/*): universe generalizations (#19153)

kim-em committed 2 years ago

13361559

chore(archive/imo): change namespace `imo` to `imoYYYY_qX` (#19152)

adomani committed 2 years ago

5f25c089

chore(*): add mathlib4 synchronization comments (#19151)

github-actions[bot] committed 2 years ago

5c1efce1

chore(*): add mathlib4 synchronization comments (#19148)

github-actions[bot] committed 2 years ago

af471b9e

chore(ring_theory/root_of_unity): move and split a file (#19144)

riccardobrasca committed 2 years ago

7fdeecc0

feat(measure_theory/measure/hausdorff): invariance instances (#19145)

eric-wieser committed 2 years ago

3d5c4a7a

feat(measure_theory/measure/hausdorff): the 1-measure of a segment is its length (#18981)

eric-wieser committed 2 years ago

571e13ca

chore(ring_theory/tensor_product): replace `is_scalar_tower` by `smul_comm_class` in `left_algebra` (#19118)

ADedecker committed 2 years ago

69b2e97a

chore(*): add mathlib4 synchronization comments (#19141)

github-actions[bot] committed 2 years ago

2ebc1d6c

chore(analysis/convex/specific_functions/deriv): remove unnecessary imports (#19140)

hrmacbeth committed 2 years ago

a1666563

chore(analysis/special_functions/exp_deriv): downgrade import (#19139)

hrmacbeth committed 2 years ago

6a5c8500

feat(number_theory/sum_two_squares): add result for general n (#19054)

MichaelStollBayreuth committed 2 years ago

34ebaffc

chore(ring_theory/derivation): split file (#19138)

kim-em committed 2 years ago

b608348f

chore(ring_theory): remove `splitting_field` dependency from `is_integrally_closed` (#19137)

Vierkantor committed 2 years ago

d35b4ff4

doc(analysis/normed_space/pi_Lp): fix corrupt synchronization header (#19134)

eric-wieser committed 2 years ago

9d013ad8

Older