inv_weightMap — Mathlib

English

The inverse of index equivalence equals the inverse of the Hom index equiv.

Русский

Обратное отображение индекса эквивалентности равно обратному отображению индексов Hom.

LaTeX

$$$ (symm P Q f).indexEquiv = (Hom.indexEquiv f.toHom)^{-1} $$$

Lean4

@[simp]
theorem inv_weightMap {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) :
    (symm P Q f).weightMap = (weightEquiv P Q f).symm :=
  rfl

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