natCast_eq_one_of_odd_of_two_eq_zero

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#natCast_eq_one_of_odd_of_two_eq_zero

← MathLib Explorer

English

If n is odd and 2 = 0 in R, then (n : R) = 1.

Русский

Если n нечётно и 2 = 0 в R, то (n : R) = 1.

LaTeX

$$$\mathrm{Odd}(n) \Rightarrow (2 : R) = 0 \Rightarrow (n : R) = 1.$$$

Lean4

theorem natCast_eq_one_of_odd_of_two_eq_zero {n : ℕ} (hn : Odd n) (h : (2 : R) = 0) : (n : R) = 1 :=
  (natCast_eq_zero_or_one_of_two_eq_zero' n h).2 hn

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

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

Разделы

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

Аффилиация

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