isUnit_algebraMap — Mathlib

English

For any r ∈ R, algebraMap R (ExteriorAlgebra R M) r is a unit in the exterior algebra iff r is a unit in R.

Русский

Для любого r ∈ R элемент algebraMap R (ExteriorAlgebra R M) r является единицей в внешней алгебре тогда и только тогда, когда r — единица в R.

LaTeX

$$$\mathrm{IsUnit}(\mathrm{algebraMap}_{R \to \mathrm{ExteriorAlgebra}}(r)) \iff \mathrm{IsUnit}(r)$$$

Lean4

theorem isUnit_algebraMap (r : R) : IsUnit (algebraMap R (ExteriorAlgebra R M) r) ↔ IsUnit r :=
  isUnit_map_of_leftInverse _ (algebraMap_leftInverse M)

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