Commit 2024-08-11 23:33 0b828955
View on Github →feat(Algebra/Group/Subgroup/Basic): inclusion_inj
(#15699)
Add the lemma
@[to_additive (attr := simp)]
lemma inclusion_inj {H K : Subgroup G} (h : H ≤ K) {x y : H} :
inclusion h x = inclusion h y ↔ x = y :=
(inclusion_injective h).eq_iff
following usual practice for injectivity lemmas. From AperiodicMonotilesLean.