Commit 2022-11-28 15:29 6d140cbf

View on Github →

feat: port Algebra.Hom.Embedding (#764) sha 76171581280d5b5d1e2d1f4f37e5420357bdc636

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/Embedding.lean

added def mulLeftEmbedding

added def mulRightEmbedding

added theorem mul_left_embedding_eq_mul_right_embedding