Commit 2026-09-03 10:12 c6928328

chore(GroupTheory): make arguments implicit in two iff lemmas (#43382) We make arguments implicit in these two iff lemmas about double coset:

lemma eq'' {a b : G} {H K : Subgroup G} : mk H K a = mk H K b ↔ setoid H K a b :=
lemma eq {H K : Subgroup G} {a b : G} :