AlgebraEvaluation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.symAlg_eq_zero_of_lift_eq_zero line 13
Source documentation
Linear functionals separate points of the symmetric algebra over an infinite field.
```
theorem symAlg_eq_zero_of_lift_eq_zero (p : SymmetricAlgebra ℂ W)
    (h : ∀ φ : Module.Dual ℂ W, SymmetricAlgebra.lift φ p = 0) : p = 0 := by
…
```

theorem OAI.Problem346.symAlg_dual_eq_zero_of_eval_eq_zero line 33

Source documentation

Evaluation at vectors separates the symmetric algebra on the dual of a finite-dimensional space.

theorem symAlg_dual_eq_zero_of_eval_eq_zero [FiniteDimensional ℂ W]
    (p : SymmetricAlgebra ℂ (Module.Dual ℂ W))
    (h : ∀ x : W, SymmetricAlgebra.lift (Module.Dual.eval ℂ W x) p = 0) : p = 0 := by
…