algebraMap_eq_one_iff — Mathlib

English

For all x ∈ R, algebraMap R (ExteriorAlgebra R M) x = 1 if and only if x = 1.

Русский

Для всех x ∈ R: algebraMap R (ExteriorAlgebra R M) x = 1 тогда и только тогда, когда x = 1.

LaTeX

$$$\mathrm{algebraMap}_{R \to \mathrm{ExteriorAlgebra}}(x) = 1 \iff x = 1$$$

Lean4

@[simp]
theorem algebraMap_eq_one_iff (x : R) : algebraMap R (ExteriorAlgebra R M) x = 1 ↔ x = 1 :=
  map_eq_one_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

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