iso₀ — Mathlib

English

For any commutative ring R and any R-module M, the 0th exterior power of M is canonically isomorphic to R as an R-module.

Русский

Для произвольного кольца R и модуля M над R нулевая внешняя степень модуля M канонически изоморфна кольцу R как R-модуль.

LaTeX

$$$$ \\bigwedge^0 M \\cong_R R $$$$

Lean4

/-- The isomorphism `M.exteriorPower 0 ≅ ModuleCat.of R R`. -/
noncomputable def iso₀ (M : ModuleCat.{u} R) : M.exteriorPower 0 ≅ ModuleCat.of R R :=
  (exteriorPower.zeroEquiv R M).toModuleIso

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