one

Mathlib.Algebra.GroupWithZero.NeZero

URI: https://scilib.ai/kg/mathlib#NeZero.one

← MathLib Explorer

English

1 ≠ 0.

Русский

1 ≠ 0.

LaTeX

$$1 \\neq 0$$

Lean4

/-- In a nontrivial monoid with zero, zero and one are different. -/
instance one : NeZero (1 : M₀) :=
  ⟨by
    intro h
    rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
    apply hx
    calc
      x = 1 * x := by rw [one_mul]
      _ = 0 := by rw [h, zero_mul]
      _ = 1 * y := by rw [h, zero_mul]
      _ = y := by rw [one_mul]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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