intCast

Mathlib.Data.Int.Cast.Lemmas

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

English

If n is odd in the integers, then its image in α is odd (for any ring α).

Русский

Если n нечетно в целых, то его образ в любом кольце α нечетен.

LaTeX

$$$ \forall {\alpha} [Ring \alpha],\forall n \in \mathbb{Z},\text{Odd}(n) \Rightarrow \text{Odd}(n : \alpha).$$$

Lean4

theorem _root_.Odd.intCast (hn : Odd n) : Odd (n : α) :=
  hn.map (castRingHom α)

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

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

Разделы

Аффилиация

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