mathlib
2f1a4aff - feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470)

Commit
4 years ago
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".
Author
Parents
Loading