mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Prove that the product of two Freiman homomorphisms/isomorphisms is a Freiman homomorphism/isomorphism. --- [](https://gitpod.io/from-referrer/)
Given two complex shapes `c : ComplexShape ι` and `c' : ComplexShape ι'` for homological complexes, an embedding from `c` to `c'` (`e : c.Embedding c'`) consists of the data...
and move `Data.Nat.Interval`/`Data.Fin.Interval` to `Order.Interval.Finset.Nat`/`Order.Interval.Finset.Fin`. --- [](https://gitpod.io/from-referrer/)
These are wrappers around the constructor and projection for `Opposite Quiver.Hom _ _`. The projection itself is reducible and with structure eta built in to defeq it seems like we...
One additivised lemma was missing a deprecation. --- [](https://gitpod.io/from-referrer/)
Definitions and basic properties of non-unital star ring homomorphisms --- [](https://gitpod.io/from-referrer/)
This tried to make the concrete category developments more uniform: whether `coe_of` was a simp lemma or not seems to have been decided differently in different files during porting. Also...
- introduce a mixin class `DFunLike.PointwiseLE`, use it to define `DFunLike.instPartialOrder`; - add a generic `DFunLike.orderEmbeddingCoe` - add `DFunLike.PointwiseLE` instances here and there. With this refactor and #13022, I'm going...
--- - [ ] depends on: #13025 [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)