linearEquivFunOnFinite_symm_single

English

For finite α, and f : α →₀ M, the inverse of the finite linear equivalence sends f to itself; i.e., the inverse map acts as identity on α →₀ M.

Русский

Для конечного α и f : α →₀ M обратное отображение линейного эквивалентного отображения повторно отобразит f в сам f.

LaTeX

$$$(linearEquivFunOnFinite R M α).symm f = f$.$$

Lean4

@[simp]
theorem linearEquivFunOnFinite_symm_single [DecidableEq α] (x : α) (m : M) :
    (linearEquivFunOnFinite R M α).symm (Pi.single x m) = single x m :=
  equivFunOnFinite_symm_single x m

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