mathlib

1073204e - feat(logic/nontrivial): function.injective.exists_ne (#3983)

feat(logic/nontrivial): function.injective.exists_ne (#3983) Add a lemma that an injective function from a nontrivial type has an argument at which it does not take a given value.