dim_ne_zero

Mathlib.RingTheory.PowerBasis

URI: https://scilib.ai/kg/mathlib#PowerBasis.dim_ne_zero

← MathLib Explorer

English

If S is nontrivial, pb.dim ≠ 0 for a PowerBasis pb of R in S.

Русский

Пусть S ненулево; тогда pb.dim ≠ 0 для PowerBasis pb над R в S.

LaTeX

$$$pb.\\mathrm{dim} \\neq 0$ under $[\\text{Nontrivial } S]$.$$

Lean4

theorem dim_ne_zero [Nontrivial S] (pb : PowerBasis R S) : pb.dim ≠ 0 := fun h =>
  not_nonempty_iff.mpr (h.symm ▸ Fin.isEmpty : IsEmpty (Fin pb.dim)) pb.basis.index_nonempty

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

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

Разделы

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

Аффилиация

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