botEquivPUnit — Mathlib

English

There is a linear isomorphism between the bottom submodule ⊥ and the one-element module PUnit as R-modules.

Русский

Существует линейное изоморфизм между нулевым подмодулем ⊥ и одноэлементным модулем PUnit как R-модулям.

LaTeX

$$$(\bot : \mathrm{Submodule}\, R M) \cong_R PUnit$$$

Lean4

/-- The bottom submodule is linearly equivalent to punit as an `R`-module. -/
@[simps]
def botEquivPUnit : (⊥ : Submodule R M) ≃ₗ[R] PUnit.{v + 1}
    where
  toFun _ := PUnit.unit
  invFun _ := 0
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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