Commit 2023-09-04 13:19 8dea0d0f

View on Github →

chore: Fix add_left_embedding_eq_add_right_embedding name (#6935) This was accidentally snake case.

Estimated changes

Modified Mathlib/Algebra/Hom/Embedding.lean

added theorem mulLeftEmbedding_eq_mulRightEmbedding

deleted theorem mul_left_embedding_eq_mul_right_embedding

Modified Mathlib/Combinatorics/Additive/SalemSpencer.lean