domCongr_toAlgHom — Mathlib

English

As above, the equality (domCongr k A e).toAlgHom = mapDomainAlgHom k A e holds.

Русский

Как выше, выполняется равенство (domCongr k A e).toAlgHom = mapDomainAlgHom k A e.

LaTeX

$$$\\big(\\mathrm{domCongr}\\ k\\;A\\;e\\big).\\mathrm{toAlgHom} = \\mathrm{mapDomainAlgHom}\\ k\\;A\\;e$$$

Lean4

@[to_additive]
theorem domCongr_toAlgHom (e : G ≃* H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _

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