English
There is a canonical equivalence between algebra homomorphisms from ExteriorAlgebra R M to A and linear maps f: M → A satisfying f(m) f(m) = 0 for all m.
Русский
Существует каноническое равенство между гомоморфизмами от ExteriorAlgebra R M в A и линейными отображениями f: M → A, удовлетворяющими условию f(m)^2 = 0 для всех m.
LaTeX
$$ExteriorAlgebra.lift : { f : M →ₗ[R] A // ∀ m, f m * f m = 0 } ≃ (ExteriorAlgebra R M →ₐ[R] A)$$
Lean4
@[macro ExteriorAlgebra.«term⋀[_]^_»]
public meta def «_aux_Mathlib_LinearAlgebra_ExteriorAlgebra_Basic___macroRules_ExteriorAlgebra_term⋀[_]^__1» : Macro✝ :=
fun
| `(⋀[$R]^$n) => ``(exteriorPower $R $n)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
