inv_coweightMap — Mathlib

English

Further properties of the inverse index equivalence in the RootPairing context.

Русский

Дополнительные свойства обратного индекса эквивалентности в контексте RootPairing.

LaTeX

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

Lean4

@[simp]
theorem inv_coweightMap {ι₂ 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).coweightMap = (coweightEquiv P Q f).symm :=
  rfl

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