map_basis_ne_zero_iff

Mathlib.LinearAlgebra.Determinant

URI: https://scilib.ai/kg/mathlib#AlternatingMap.map_basis_ne_zero_iff

← MathLib Explorer

English

For finite ι, Ne(f e, 0) is equivalent to Ne(f, 0).

Русский

Для конечного ι, неравенство f e ≠ 0 эквивалентно f ≠ 0.

LaTeX

$$f e ≠ 0 ↔ f ≠ 0$$

Lean4

theorem map_basis_ne_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) : f e ≠ 0 ↔ f ≠ 0 :=
  not_congr <| f.map_basis_eq_zero_iff e

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru