Theorems · Theorem · group theory

map_ne_zero_iff

∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : Zero R] [inst_1 : Zero S] [inst_2 : FunLike F R S]
  [ZeroHomClass F R S] (f : F), Function.Injective ⇑f → ∀ {x : R}, f x ≠ 0 ↔ x ≠ 0

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

24 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

ZeroZeroFunLikeZeroHomClass