mathlib
mathlib copied to clipboard
leanprover-community
Lean 3's obsolete mathematical components library: please use mathlib4
--- [](https://gitpod.io/from-referrer/) - [x] depends on: #16928
These all came up while preparing to introduce the definition of ergodic maps but it seems better to PR them separately. --- [](https://gitpod.io/from-referrer/)
Some of this is necessary to define the (closed) C⋆-algebra generated by a single element, which is in turn necessary to define the continuous functional calculus. --- [](https://gitpod.io/from-referrer/)
Construction of the cross-product on an oriented real inner product space of dimension 3. Formalized as part of the Sphere Eversion project. --- [](https://gitpod.io/from-referrer/) - [x] depends on:...
We define functions of bounded variation. We show that such functions are a difference of monotone functions, and deduce that they are differentiable almost everywhere. This applies in particular to...
A multiplicative action of `N` on `R` and a ring homomorphism `K →+* N` induce a multiplicative action of `K` on `R`. I need this for my study of the...
This PR introduces variations on the statements of simplicial relations which makes it easier to use. This is demonstrated in `algebraic_topology.dold_kan.faces`. The attribute `reassoc` is also added to the simplicial...
* From the sphere eversion project * Needed for computing derivatives of the parametric interval integral Co-authored by: Patrick Massot [[email protected]](mailto:[email protected]) --- [](https://gitpod.io/from-referrer/)
Redefine the various `noncomm_prod`s using `set.pairwise`. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the trivial `i...
This is one of the two contravariant functors involved in Gelfand duality. --- [](https://gitpod.io/from-referrer/)
Metadata
Owner
Metadata
Lean 3's obsolete mathematical components library: please use mathlib4