Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 03:36 2f1a4aff

View on Github →

feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470) This introduces the notation A →ₙₐ[R] B for non_unital_alg_hom R A B to mirror that of non_unital_ring_hom R S as R →ₙ+* S from #13430. Here, the stands for "non-unital".

Estimated changes