nontrivial

Mathlib.Algebra.Field.IsField

URI: https://scilib.ai/kg/mathlib#IsField.nontrivial

English

A field has no zero divisors; in particular, cancellation laws hold: if a ≠ 0 and ab = ac, then b = c.

Русский

У поля нет нулевых делителей; в частности верны правила отмены: если a ≠ 0 и ab = ac, то b = c.

LaTeX

$$$IsField\,R \Rightarrow IsDomain\,R$$$

Lean4

@[simp]
theorem nontrivial {R : Type u} [Semiring R] (h : IsField R) : Nontrivial R :=
  ⟨h.exists_pair_ne⟩

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

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

Разделы

Аффилиация

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