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.

Estimated changes