inv_hom_hom — Mathlib

English

Symmetric statement of hom_inv_hom: the composite of inverse and forward maps is the identity on the target.

Русский

Симметричное утверждение: композиция обратного и прямого отображения равна тождественному отображению на целевом объекте.

LaTeX

$$$\\text{inv\_hom\_hom} : f:\\ M \\cong N \\Rightarrow f.inv.hom \\circ f.hom.hom = \\mathrm{id}_{N.V}$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_hom_hom {M N : Action V G} (f : M ≅ N) : f.inv.hom ≫ f.hom.hom = 𝟙 N.V := by
  rw [← comp_hom, Iso.inv_hom_id, id_hom]

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