Theorems · Theorem · number theory

Odd.map

∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : Semiring β] {a : α}
  [inst_2 : FunLike F α β] [RingHomClass F α β] (f : F), Odd a → Odd (f a)

Defined in

Mathlib.Algebra.Ring.Parity

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

SemiringSemiringFunLikeRingHomClass