coe_comapSubgroup — Mathlib

English

For an isomorphism e: G ≃* H, the two constructions comapSubgroup e and Subgroup.comap e.toMonoidHom coincide; they define the same preimage lattice via the underlying monoid homomorphism.

Русский

Для изоморфизма e: G ≃* H две конструкции comapSubgroup e и Subgroup.comap e.toMonoidHom совпадают и задают одну и ту же решётку предобразов через соответствующий моноид-гомоморфизм.

LaTeX

$$$\\operatorname{comapSubgroup}(e) = \\operatorname{Subgroup.comap}(e^{\\mathrm{toMonoidHom}})$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_comapSubgroup (e : G ≃* H) : comapSubgroup e = Subgroup.comap e.toMonoidHom :=
  rfl

Похожие утверждения