map_basis_eq_zero_iff — Mathlib

English

For finite ι, an alternating map f vanishes on the basis e if and only if f is the zero map.

Русский

Для конечного ι, если f равно нулю на базисе e, то f равно нулю как отображение, и наоборот.

LaTeX

$$f e = 0 ↔ f = 0$$

Lean4

@[simp]
theorem map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
  ⟨fun h => by
    cases nonempty_fintype ι
    letI := Classical.decEq ι
    simpa [h] using f.eq_smul_basis_det e, fun h => h.symm ▸ AlternatingMap.zero_apply _⟩

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