Commit 2024-11-13 12:57 6a85082c
View on Github →chore: rename IsEmbedding.inj to IsEmbedding.injective (#18921)
All other fields have decent names. Furthermore, inj as a name is reserved to mean f a = f b ↔ a = b.
chore: rename IsEmbedding.inj to IsEmbedding.injective (#18921)
All other fields have decent names. Furthermore, inj as a name is reserved to mean f a = f b ↔ a = b.