mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
In principle, `Fintype.univ_ofSubsingleton` could be a `simp` theorem but it applies to any occurence of `univ` and requires unification of the (possibly very complex) `Fintype` instances. It appears to not...
This PR defines `CFC.log` as `cfc Real.log`, and shows its basic properties, such as the fact that it's the inverse of `NormedSpace.exp ℝ`. Along the way, we also show that...
We add the class `ContinuousAlgHom` for continuous algebra homomorphisms. Co-authored-by: Antoine Chambert-Loir --- [](https://gitpod.io/from-referrer/)
Line derivative of a quadratic form is given by its polar bilinear form. --- [](https://gitpod.io/from-referrer/)
Split off `Infinitude` and `Int` from `Nat/Primes/Defs` and `...Basic`, leading to more opportunities for optimizing imports. Now, only 7 end node modules still import the full `Prime.lean`. --- - [...
We already have that category of commutative rings has colimits, the same construction works for category of rings. --- [](https://gitpod.io/from-referrer/)
add Dershowitz-Manna Ordering and Theorem for Multisets Co-authored-by: Malvin Gattinger --- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Dershowitz-Manna.20Ordering.20theorem/near/434390710 [](https://gitpod.io/from-referrer/)
This PR proves that the properties `PreservesSheafification` and `WEqualsLocallyBijective` hold for an essentially small site if they hold for an equivalent small site. --- [](https://gitpod.io/from-referrer/)
Prove that a function that is bounded and a.e. continuous within a box is integrable on that box. This generalizes integrable_of_continuousOn. As an intermediate step, define the oscillation of a...
The mates bijection between natural transformations inhabiting a certain dual pairs of squares (the duality in the sense of a parallel pair of adjunctions) can be defined in a more...
