mathlib

mathlib copied to clipboard

The distance between `λ _, a` and `λ _, b` is less than the distance between `a` and `b`. --- [](https://gitpod.io/from-referrer/)

YaelDillies

Add `function.extend_apply_of_unique` which allows to rewrite `function.extend f g e (f a) = g a` not only when `f` is injective, what `function.extend_apply` does, but when `f a = f...

AntoineChambert-Loir

Version of `exists_seq_strict_mono_tendsto`/`exists_seq_strict_anti_tendsto` strengthened to `nhds_within`. --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(algebra/ring/aut): add apply_mul_semiring_action & mul_semiring_action.to_ring_aut

4

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

mkaratarakis

and three easy lemmas --- [](https://gitpod.io/from-referrer/)

YaelDillies

Simple lemmas about `directed`. --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(probability/independence): Kolmogorov's 0-1 law

1

We prove that any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1. --- - [x] depends on: #16759 [](https://gitpod.io/from-referrer/)

RemyDegenne

A few lemmas about emetric spaces and `nhds_within`. --- Note, I don't need those lemmas. I just found myself writing them before figuring out another approach. [](https://gitpod.io/from-referrer/)

YaelDillies

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring

5

We define the finite adèle ring of a Dedekind domain and show that it is a commutative ring. --- [](https://gitpod.io/from-referrer/)

mariainesdff

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

kex-y