all

Mathlib.Algebra.CharP.Invertible

URI: https://scilib.ai/kg/mathlib#Even.all

← MathLib Explorer

English

In a division semiring K with characteristic zero, the element 2 ∈ K is invertible.

Русский

В дивизионном полукольце K с характеристикой ноль, элемент 2 ∈ K обратим.

LaTeX

$$$\text{Invertible}(2)\,\text{in } K$$$

Lean4

/-- When two is invertible, every element is `Even`. -/
@[simp]
theorem all [Semiring R] [Invertible (2 : R)] (a : R) : Even a :=
  .of_isUnit_two (isUnit_of_invertible _) _

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

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

Разделы

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

Аффилиация

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