leanprover-community/mathlib

Pull Requests Commits

feat(*): generalise+add algebraic instances (#18947)

ericrbg committed 3 years ago

949dc57e

feat(data/real/ennreal): interactions between infi/supr and to_nnreal/to_real (#18946)

collares committed 3 years ago

c1686dff

feat(field_theory/adjoin,normal): `field_range` lemmas (#18959)

tb65536 committed 3 years ago

d4437c68

feat(field_theory/intermediate_field): Inhabited instance (#18956)

tb65536 committed 3 years ago

c596622f

feat(probability/kernel/basic): integrals of basic kernels (#18961)

RemyDegenne committed 3 years ago

a9545e8a

feat(probability/kernel/basic): add `kernel.comap_right` and `kernel.piecewise` (#18917)

RemyDegenne committed 3 years ago

63decdb8

feat(algebra/order/group/order_iso): add `order_iso.div_{left,right}` (#18968)

urkud committed 3 years ago

6632ca20

feat(analysis/calculus/deriv): `polynomial.aeval` lemmas (#18945)

eric-wieser committed 3 years ago

f81174bd

feat(order/category): Category of finite distributive lattices (#11677)

YaelDillies committed 3 years ago

937b1c59

refactor(data/is_R_or_C,analysis/inner_product_space): review API (#18919)

urkud committed 3 years ago

3f655f52

refactor(linear_algebra/dual): make `module.dual` reducible (#18963)

urkud committed 3 years ago

b1c01758

feat(measure_theory/measure/stieltjes): add measure_Iic, measure_Ici, measure_univ (#18884)

RemyDegenne committed 3 years ago

08e1d8d4

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

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

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

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

Newer Older