mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
- `TensorProduct.congr_symm` which states `(TensorProduct.congr f g).symm = TensorProduct.congr f.symm g.symm` - `TensorProduct.coe_congr_(left|right)_refl`: relates `TensorProduct.congr` and `LinearMap.(l|r)Tensor` --- [](https://gitpod.io/from-referrer/)
This PR allows the names to be clearly distinguished from versions that do not require positivity assumptions, but also become too long. Due to name conflicts, some similar lemmas have...
This PR defines the type `Triangulated.Subcategory C` when `C` is a pretriangulated category. It also introduces a type class `Set.RespectsIso` for set of objects in a category `C` that is...
add a type of Katetov maps (one point extensions of a metric) and related notation and FunLike coercions. --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
Adds new syntax for sum/product big operators for `∑ x ∈ s, f x`. The set `s` can either be a `Finset` or a `Set` with a `Fintype` instance, in...
This is a draft PR which will be split into many chunks for final submission - Abstract functional-equation argument for Mellin transforms - Refactor Riemann zeta using this - Hurwitz...
In this file, it is shown that if a class of morphisms `W` in a pretriangulated category is compatible with the triangulation and has a left calculus of fractions, then...