natCast

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Odd.natCast

English

If n is odd, then its image in any semiring R is odd.

Русский

Если n нечётно, то образ n в любом полукольце R нечётен.

LaTeX

$$$\forall R\ [\operatorname{Semiring} R],\ \operatorname{Odd}(n) \rightarrow \operatorname{Odd}(n:\,R)$$$

Lean4

theorem natCast {R : Type*} [Semiring R] {n : ℕ} (hn : Odd n) : Odd (n : R) :=
  hn.map <| Nat.castRingHom R

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

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

Разделы

Аффилиация

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