map

Mathlib.Algebra.Ring.Parity

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

English

Let f be a ring homomorphism. If a is odd, then f(a) is odd.

Русский

Пусть f — кольцевой гомоморфизм. Если a нечётно, то f(a) нечётно.

LaTeX

$$$\operatorname{Odd} a \rightarrow \operatorname{Odd}(f a)$$$

Lean4

theorem map [FunLike F α β] [RingHomClass F α β] (f : F) : Odd a → Odd (f a) := by rintro ⟨a, rfl⟩;
  exact ⟨f a, by simp [two_mul]⟩

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

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

Разделы

Аффилиация

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