leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/RD_aux_kernel' into RD_disintegration

RemyDegenne committed 3 years ago

a3273f1b

RemyDegenne committed 3 years ago

51ea4c00

Merge remote-tracking branch 'origin/master' into RD_integral_kernel

RemyDegenne committed 3 years ago

7e0ae5f8

Merge remote-tracking branch 'origin/master' into RD_aux_kernel

RemyDegenne committed 3 years ago

718f0b08

chore(probability/kernel/basic): split into three files (#18957)

RemyDegenne committed 3 years ago

483dd86c

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

github-actions[bot] committed 3 years ago

b5ad1414

move, rename, reorganize

RemyDegenne committed 3 years ago

0443123d

feat(algebra/order/to_interval_mod): notation for `add_comm_group.modeq` (#18955)

eric-wieser committed 3 years ago

ba2eb704

feat(order/category): Free functor `Lat ⥤ BddLat` (#18949)

YaelDillies committed 3 years ago

75810309

integral of comp_prod

RemyDegenne committed 3 years ago

5e1154bc

feat(algebra/order/to_interval_mod): symmetric variants of lemmas (#18942)

eric-wieser committed 3 years ago

4c8f86bd

chore(algebra/order/lattice_group): remove redundant instance (#18951)

kim-em committed 3 years ago

db07e6fe

feat(order/category): Forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` (#18948)

YaelDillies committed 3 years ago

fa4a805d

RemyDegenne committed 3 years ago

0694ec74

RemyDegenne committed 3 years ago

d8efcc39

Merge remote-tracking branch 'origin/master' into RD_disintegration

RemyDegenne committed 3 years ago

c69a0d18

RemyDegenne committed 3 years ago

31615616

doc(measure_theory): Fix some names and docstrings (#18910)

Felix-Weilacher committed 3 years ago

3905fa80

feat(number_theory/number_field/units): add is_unit_iff_norm (#18866)

xroblot committed 3 years ago

00f91228

chore(data/is_R_or_C/basic): rename `conj_mul_eq_norm_sq_left` to `conj_mul` (#18939)

urkud committed 3 years ago

25580801

feat(field_theory/intermediate_field): Add lemma for the `field_range` of `val` (#18940)

tb65536 committed 3 years ago

efed3cad

chore(number_theory/modular_forms/slash_invariant_forms): golf and rename (#18933)

eric-wieser committed 3 years ago

738054fa

feat(ring_theory/localization/away) : Add `num_denom` section (#18830)

faenuccio committed 3 years ago

570e9f48

chore(ring_theory/derivation): generalize tower instance (#18937)

eric-wieser committed 3 years ago

26ae6f67

chore(ring_theory/ideal/quotient): add missing smul compatibility instances (#18934)

eric-wieser committed 3 years ago

2f39bcbc

feat(data/is_R_or_C/basic): drop 2 fields, golf (#18931)

urkud committed 3 years ago

338fe44f

chore(probability/kernel/basic): make the function argument of kernel.deterministic explicit (#18930)

RemyDegenne committed 3 years ago

caf83ba4

chore(probability/kernel/composition): swap the order of the arguments of prod_mk_left (#18929)

RemyDegenne committed 3 years ago

698c80e9

chore(analysis/inner_product_space/basic): golf the proof of Cauchy-Schwarz (#18938)

urkud committed 3 years ago

07992a1d

feat(field_theory/ax_grothendieck): Ax-Grothendieck for algebraic extensions of finite fields (#18479)

ChrisHughes24 committed 3 years ago

4e529b03

Newer Older