iso₁_hom_apply — Mathlib

English

The homomorphism part of the iso1 isomorphism sends the canonical generator to the corresponding element of M.

Русский

Гомоморфная часть изоморфизма iso1 отправляет канонический генератор в соответствующий элемент M.

LaTeX

$$$$ (\\operatorname{iso}_1 M)_{\\mathrm{hom}}(e) = m_0 $$$$

Lean4

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

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