mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
--- [](https://gitpod.io/from-referrer/)
Redefine `BilinForm.IsRefl`, `BilinForm.IsAlt` and `BilinForm.IsSymm` in terms of `LinearMap.IsRefl` and `LinearMap.IsSymm`. This is a step towards eventually replacing `BilinForm`. --- - [x] depends on: #10422 [](https://gitpod.io/from-referrer/)
This PR gives a convenient characterisation of the Scott Topology for a Complete Linear Order --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
We show that if a sub basis is closed under finite intersections and contains the universal set then it is a basis for a topology. As a corollary, if a...
Definitions and basic properties of non-unital star subsemirings --- This file heavily copies `Mathlib.Algebra.Star.NonUnitalSubalgebra`, so I'm happy to assign the copyright to @j-loreaux if that's the appropriate thing to do....
Loosens the hypothesis of `LinearEquiv.arrowCongr` to get an `R`-linear equivalence between spaces of `R₁`-linear maps. This is needed for #9334. --- [](https://gitpod.io/from-referrer/)
Generalise `compl₂` and `compl₁₂` for left composition with maps which are linear over different rings in the first and second variable. Needed for #9334 --- [](https://gitpod.io/from-referrer/)
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Unscoping.20big.20operators Also, we change the notation for [`CategoryTheory.Limits.piObj`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/Products.html#CategoryTheory.Limits.piObj) from `∏ f` to `∏ᶜ f`. --- [](https://gitpod.io/from-referrer/)
--- - [ ] depends on: #12610 [](https://gitpod.io/from-referrer/)