nontrivial

Mathlib.RingTheory.Valuation.RankOne

URI: https://scilib.ai/kg/mathlib#Valuation.RankOne.nontrivial

English

There exists r in R with v(r) not equal to 0 and not equal to 1.

Русский

Существует элемент r из R such that v(r) не равно 0 и не равно 1.

LaTeX

$$$\exists r\in R:\; v(r) \neq 0 \wedge v(r) \neq 1.$$$

Lean4

theorem nontrivial : ∃ r : R, v r ≠ 0 ∧ v r ≠ 1 :=
  IsNontrivial.exists_val_nontrivial

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

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

Разделы

Аффилиация

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