Mathlib Map

Theorems · Theorem · order theory

map_ne_zero_iff_ne_zero

∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupNormClass F α β] (f : F) {x : α}, f x ≠ 0 ↔ x ≠ 0
Defined in
Mathlib.Algebra.Order.Hom.Basic
Cited by
1 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext
Assumes
FunLikeAddGroupAddCommMonoidPartialOrderAddGroupNormClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

map_pos_of_ne_zero · cited by 3map_pos_of_ne_zeroDFunLike.coe · cited by 62936DFunLike.coeAddCommMonoid · cited by 12281AddCommMonoidPartialOrder · cited by 6410PartialOrderAddGroup · cited by 4410AddGroupFunLike · cited by 2560FunLikeIff.not · cited by 489Iff.notAddGroupNormClass · cited by 6AddGroupNormClassmap_eq_zero_iff_eq_zero · cited by 1map_eq_zero_iff_eq_zeromap_ne_zero_iff_ne_zeroCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.