leanprover-community/mathlib3

Pull Requests Commits

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

hrmacbeth committed 3 years ago

533f62f4

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

kim-em committed 3 years ago

13361559

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

adomani committed 3 years ago

5f25c089

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

github-actions[bot] committed 3 years ago

5c1efce1

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

github-actions[bot] committed 3 years ago

af471b9e

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

riccardobrasca committed 3 years ago

7fdeecc0

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

eric-wieser committed 3 years ago

3d5c4a7a

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

eric-wieser committed 3 years ago

571e13ca

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

ADedecker committed 3 years ago

69b2e97a

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

github-actions[bot] committed 3 years ago

2ebc1d6c

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

hrmacbeth committed 3 years ago

a1666563

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

hrmacbeth committed 3 years ago

6a5c8500

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

MichaelStollBayreuth committed 3 years ago

34ebaffc

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

kim-em committed 3 years ago

b608348f

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

Vierkantor committed 3 years ago

d35b4ff4

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

eric-wieser committed 3 years ago

9d013ad8

chore(field_theory/ratfunc): use `section` instead of `omit/include` (#19133)

adomani committed 3 years ago

67237461

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

github-actions[bot] committed 3 years ago

599fffe7

refactor(number_theory/liouville/liouville_number): review API, golf (#19126)

urkud committed 3 years ago

04e80bb7

feat (number_theory/zeta_function): relate to Dirichlet series (#19131)

loefflerd committed 3 years ago

cca40788

feat(analysis/schwartz_space): Multiplication of Schwartz function and functions of temperate growth (#18649)

mcdoll committed 3 years ago

e137999b

feat(probability/kernel/cond_distrib): regular conditional probability distributions (#19090)

RemyDegenne committed 3 years ago

00abe069

feat(linear_algebra/matrix/adjugate): add `det_eq_sum_mul_adjugate_row` (#19117)

eric-wieser committed 3 years ago

a99f8522

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

github-actions[bot] committed 3 years ago

61b5e275

chore(field_theory/finite/basic): move a lemma (#19130)

riccardobrasca committed 3 years ago

12a85fac

chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129)

adomani committed 3 years ago

32837559

feat(linear_algebra/matrix/charpoly/eigs): det and trace are product and sum of eigenvalues (#19079)

MohanadAhmed committed 3 years ago

48dc6abe

feat(ring_theory/polynomial/hermite): proof of explicit formula for Hermite polynomial coefficients (#19044)

jakelev committed 3 years ago

938d3db9

feat(data/set/ncard): noncomputable set cardinality (#18576)

apnelson1 committed 3 years ago

74c2af38

refactor(analysis/calculus/darboux): review API (#19125)

urkud committed 3 years ago

9a1ffe49

Newer Older