symm_comapSubgroup — Mathlib

English

The inverse of the lattice isomorphism comapSubgroup e is the lattice isomorphism comapSubgroup e.symm; equivalently, (comapSubgroup e).symm = comapSubgroup e.symm.

Русский

Обратная тождественная к порядковому тождеству comapSubgroup e — это comapSubgroup e.symm; то есть (comapSubgroup e).symm = comapSubgroup e.symm.

LaTeX

$$$\\big(\\operatorname{comapSubgroup}(e)\\big)^{-1} = \\operatorname{comapSubgroup}(e^{-1})$$$

Lean4

@[to_additive (attr := simp)]
theorem symm_comapSubgroup (e : G ≃* H) : (comapSubgroup e).symm = comapSubgroup e.symm :=
  rfl

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