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

modified def unitization.lift
modified theorem non_unital_alg_hom.coe_comp
modified theorem non_unital_alg_hom.coe_one
modified theorem non_unital_alg_hom.coe_zero
modified theorem non_unital_alg_hom.ext
modified theorem non_unital_alg_hom.ext_iff
modified theorem non_unital_alg_hom.map_add
modified theorem non_unital_alg_hom.map_mul
modified theorem non_unital_alg_hom.map_smul
modified theorem non_unital_alg_hom.map_zero
modified theorem non_unital_alg_hom.mk_coe
modified def free_lie_algebra.mk