English
If H = K are equal subgroups of G, then there is a canonical identity isomorphism between them, i.e., a MulEquiv between their underlying membership subtypes that is the identity on elements.
Русский
Если H=K — равныие подгруппы G, то существует каноническое тождественное изоморфизм между ними, т.е. MulEquiv между их множествами элементов, действующее как тождество на элементах.
LaTeX
$$$H = K \\Rightarrow \\operatorname{MulEquiv}(\\mathrm{Subtype}\\,\\{x\\in H\\})\\cong \\mathrm{Subtype}\\,\\{x\\in K\\}$$$
Lean4
/-- Makes the identity isomorphism from a proof two subgroups of a multiplicative
group are equal. -/
@[to_additive /-- Makes the identity additive isomorphism from a proof
two subgroups of an additive group are equal. -/
]
def subgroupCongr (h : H = K) : H ≃* K :=
{ Equiv.setCongr <| congr_arg _ h with map_mul' := fun _ _ => rfl }
