zero_ne_one

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.zero_ne_one

English

The zero element in CauSeq.Completion is not equal to the multiplicative unit.

Русский

Нуль в CauSeq.Completion не равен единице умножения.

LaTeX

$$(0 : CauSeq abv) ≠ 1$$

Lean4

theorem zero_ne_one : (0 : (Cauchy abv)) ≠ 1 := fun h => cau_seq_zero_ne_one <| mk_eq.1 h

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

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

Разделы

Аффилиация

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