mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Summary of the changes: - change definitions to make [lowerSemicontinuous_iff_isClosed_preimage](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Semicontinuous.html#lowerSemicontinuous_iff_isClosed_preimage) true without assuming `LinearOrder`, so that semicontinuity corresponds to continuity for lower/upper order topology on the codomain. See discussion on...
... in lemma names and section names in order to follow the naming convention. --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
Most of the theory in `LinearAlgebra/QuadraticForm/Basic` also holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map. To keep this PR...
Proves that in a polynomial ring in n variables over a commutative ring, the subalgebra of symmetric polynomials is freely generated by the first n elementary symmetric polynomials. This is...
--- I don't understand why linter fails. [](https://gitpod.io/from-referrer/)
Add several properties of the $X$-adic valuation on the ring $K[[X]]$ when $K$ is a field. It depends on #13065. Co-authored-by: María Inés de Frutos-Fernández @mariainesdff
We show that Eisenstein Series are MDifferentiable - [x] depends on: #10377 - [x] depends on: #11244 --- [](https://gitpod.io/from-referrer/)
Add two lemmas on the multiplicity of normalized factors in relation to principal ideals and the cardinality of associates. Co-authored-by: María Inés de Frutos-Fernández @mariainesdff --- [](https://gitpod.io/from-referrer/)
Add two lemmas about the element `X` as term of the normalization monoid $k[[X]]$ for a field `k`. Co-authored-by: María Inés de Frutos-Fernández @mariainesdff