natCast_eq_zero_of_even_of_two_eq_zero

Mathlib.Algebra.Ring.Parity

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\text{hn} : \mathrm{Even}(n) \land (2 : R) = 0 \Rightarrow (n : R) = 0.$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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