alternatingMapCongrRight — Mathlib

English

Two alternating maps that agree on all distinct basis-vector inputs are equal.

Русский

Две чередующиеся карты, которые совпадают на всех независимых базисных векторах, равны.

LaTeX

$$f = g given (basis inputs) implies equality$$

Lean4

/-- An isomorphism of multilinear maps given an isomorphism between their codomains.

This is `Linear.compAlternatingMap` as an isomorphism,
and the alternating version of `LinearEquiv.multilinearMapCongrRight`. -/
@[simps!]
def alternatingMapCongrRight (e : N'' ≃ₗ[R'] N₂'') : M'' [⋀^ι]→ₗ[R'] N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N₂'')
    where
  toFun f := e.compAlternatingMap f
  invFun f := e.symm.compAlternatingMap f
  map_add' _ _ := by ext; simp
  map_smul' _ _ := by ext; simp
  left_inv _ := by ext; simp
  right_inv _ := by ext; simp

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