iso₀_hom_apply — Mathlib

English

The canonical isomorphism map from the 0th exterior power to R sends the distinguished generator to 1.

Русский

Каноническое отображение из нулевой внешней степени в R отправляет выделенный генератор в единицу.

LaTeX

$$$$ (\\operatorname{iso}_0 M)_{\\mathrm{hom}}(e_0) = 1 $$$$

Lean4

@[simp]
theorem iso₀_hom_apply {M : ModuleCat.{u} R} (f : Fin 0 → M) : (iso₀ M).hom (mk f) = 1 :=
  exteriorPower.zeroEquiv_ιMulti _

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