Theorem: Subgroup.coe_eq_one (LeanCamCombi/Kneser/Mathlib.lean)

State before:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
⊢ ↑s = ↑⊥ ↔ ↑s = 1
Tactic:
rfl
State after:
no goals