mathlib4

mathlib4 copied to clipboard

bench: lean4#3473

2

--- [](https://gitpod.io/from-referrer/)

thorimur

Update lean-toolchain for testing https://github.com/leanprover/lean4

2

--- [](https://gitpod.io/from-referrer/)

kmill

refactor: `reduceOption_length_le`

4

Reproves `reduceOption_length_eq_iff` and `reduceOption_length_le` with new auxiliary lemmas - primarily `length_eq_reduceOption_length_add_filter_none`. --- [](https://gitpod.io/from-referrer/)

BoltonBailey

WiP: Introduces the Lawson Topology to Mathlib --- [](https://gitpod.io/from-referrer/)

mans0954

feat(LightCondensed): the functor from `TopCat`

1

--- - [ ] depends on: #10412 [](https://gitpod.io/from-referrer/)

dagurtomas

chore(Data/List/Enum): move from `Basic`

1

--- [](https://gitpod.io/from-referrer/)

urkud

refactor(LinearAlgebra/BilinForm): Remove `structure BilinForm` from Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

3

Remove `structure BilinForm` from `LinearAlgebra/BilinearForm/Basic` and migrate all of `_root_.BilinForm` to `LinearMap.BilinForm` Closes: #10553 This isn't the end of the story, as there's still a lot of overlap between `LinearAlgebra/BilinearForm`...

mans0954

feat(Probability/Kernel): disintegration of finite kernels

4

Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is countable or `β` has a countably generated...

RemyDegenne

Also, these `simp` calls are better compatible with a future refactor using `FunLike` for measures. --- [](https://gitpod.io/from-referrer/)

urkud

feat: `NNRat.cast`

1

Define the canonical coercion from the nonnegative rationals to any division semiring. From LeanAPAP --- - [x] depends on: #11202 - [x] depends on: #11453 - [ ] depends on:...

YaelDillies