leanprover-community/mathlib

Pull Requests Commits

feat(data/finset/lattice): Distributivity lemmas (#18611)

YaelDillies committed 3 years ago

2d44d682

feat(algebra/order/to_interval_mod): add circular_order instance for add_circle (#17743)

eric-wieser committed 3 years ago

213b0cff

feat(probability/kernel/measurable_integral): the integral against a kernel is strongly measurable (#18974)

RemyDegenne committed 3 years ago

28b2a92f

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

github-actions[bot] committed 3 years ago

a2706b55

feat(number_theory/diophantine_approximation): add Legendre's thm on rat'l approximations (#18460)

MichaelStollBayreuth committed 3 years ago

e25a3174

refactor(algebra): Redefine `a ≡ b [PMOD p]` (#18958)

YaelDillies committed 3 years ago

a07d7509

feat(number_theory/pell): add def and properties of fundamental solutions (#18901)

MichaelStollBayreuth committed 3 years ago

0b20dffb

chore(algebra/order/absolute_value): remove unneeded imports (#18978)

kim-em committed 3 years ago

0013240b

chore(representation_theory/group_cohomology): use `fin.cast_succ` instead of coe (#18950)

eric-wieser committed 3 years ago

cc5dd624

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

github-actions[bot] committed 3 years ago

7d34004e

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

Newer Older