ι_ne_one — Mathlib

English

If R is nontrivial, then for every x ∈ M, ι_R x ≠ 1 in ExteriorAlgebra.

Русский

Если R ненулевое, то для любого x ∈ M, ι_R x не равно 1 в ExteriorAlgebra.

LaTeX

$$$\iota_R x \neq 1 \quad \text{for all } x \in M \quad \text{when } R \text{ nontrivial}$$$

Lean4

@[simp]
theorem ι_ne_one [Nontrivial R] (x : M) : ι R x ≠ 1 :=
  by
  rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]
  exact one_ne_zero ∘ And.right

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