nontrivial

Mathlib.RingTheory.Algebraic.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.IsAlgebraic.nontrivial

English

If A is algebraic over R (i.e., Algebra.IsAlgebraic R A holds), then the base ring R is nontrivial.

Русский

Если A алгебраична над R, то R не тривиально.

LaTeX

$$$ IsAlgebraic R A \to Nontrivial R $$$

Lean4

theorem nontrivial [alg : Algebra.IsAlgebraic R A] : Nontrivial R :=
  (alg.1 0).nontrivial

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

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

Разделы

Аффилиация

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