leanprover-community/mathlib

Pull Requests Commits

remove irrelevant

alexjbest committed 2 years ago

64bad0c7

alexjbest committed 2 years ago

3e46872e

alexjbest committed 2 years ago

c65a8423

dont change lib

alexjbest committed 2 years ago

08e8db24

alexjbest committed 2 years ago

3f131ae0

alexjbest committed 2 years ago

2fd6a29f

alexjbest committed 2 years ago

8e35c775

feat(analysis/normed/order/lattice): add has_solid_norm (#18554)

xroblot committed 2 years ago

5dc275ec

chore(topology/instances/ennreal): missing smul lemmas (#18980)

eric-wieser committed 2 years ago

ec4b2eeb

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

YaelDillies committed 2 years ago

2d44d682

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

eric-wieser committed 2 years ago

213b0cff

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

RemyDegenne committed 2 years ago

28b2a92f

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

leanprover-community-bot committed 2 years ago

a2706b55

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

MichaelStollBayreuth committed 2 years ago

e25a3174

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

YaelDillies committed 2 years ago

a07d7509

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

MichaelStollBayreuth committed 2 years ago

0b20dffb

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

kim-em committed 2 years ago

0013240b

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

eric-wieser committed 2 years ago

cc5dd624

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

leanprover-community-bot committed 2 years ago

7d34004e

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

ericrbg committed 2 years ago

949dc57e

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

collares committed 2 years ago

c1686dff

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

tb65536 committed 2 years ago

d4437c68

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

tb65536 committed 2 years ago

c596622f

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

RemyDegenne committed 2 years ago

a9545e8a

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

RemyDegenne committed 2 years ago

63decdb8

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

urkud committed 2 years ago

6632ca20

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

eric-wieser committed 2 years ago

f81174bd

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

YaelDillies committed 2 years ago

937b1c59

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

urkud committed 2 years ago

3f655f52

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

urkud committed 2 years ago

b1c01758

Older