Commit 2024-09-04 01:36 7c21c720

feat(Algebra/Group/Submonoid/Operations): injective_codRestrict (#15700) Add a lemma MonoidHom.injective_codRestrict

@[to_additive (attr := simp)]
lemma injective_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S)
    (h : ∀ x, f x ∈ s) : Function.Injective (f.codRestrict s h) ↔ Function.Injective f :=

whose proof is taken from that of AlgHom.injective_codRestrict. From AperiodicMonotilesLean.