dim_pos

Mathlib.RingTheory.PowerBasis

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

English

If S is nontrivial, then pb.dim > 0 for a PowerBasis pb.

Русский

Если S ненулево, то pb.dim > 0 для PowerBasis pb.

LaTeX

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

Lean4

theorem dim_pos [Nontrivial S] (pb : PowerBasis R S) : 0 < pb.dim :=
  Nat.pos_of_ne_zero pb.dim_ne_zero

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

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

Разделы

Аффилиация

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