Theorems · Theorem · group theory

MonoidWithZeroHom.map_ite_one_zero

∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] {F : Type u_7}
  [inst_2 : FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [inst_4 : Decidable p],
  f (if p then 1 else 0) = if p then 1 else 0

Defined in

Mathlib.Algebra.GroupWithZero.Hom

Cited by

10 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

MulZeroOneClassMulZeroOneClassFunLikeMonoidWithZeroHomClassDecidable