Theorems · Theorem · group theory
map_eq_zero
∀ {G₀ : Type u_3} {M₀' : Type u_4} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : MulZeroOneClass M₀']
[Nontrivial M₀'] [inst_3 : FunLike F G₀ M₀'] [MonoidWithZeroHomClass F G₀ M₀'] (f : F) {a : G₀}, f a = 0 ↔ a = 0- Cited by
- 10 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- Nontrivialstatement and proof · cited by 2,416
- GroupWithZerostatement and proof · cited by 691
- MulZeroOneClassstatement and proof · cited by 184
- not_iff_notproof · cited by 159
- MonoidWithZeroHomClassstatement and proof · cited by 37
- map_ne_zeroproof · cited by 20
Cited by10
Results whose statement or proof uses this declaration.
- Valuation.zero_iffproof · cited by 9
- IsIntegralClosure.isFractionRing_of_finite_extensionproof · cited by 8
- NumberField.Units.dirichletUnitTheorem.seq_nextproof · cited by 3
- NNReal.exists_lt_of_strictMonoproof · cited by 2
- MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_leproof · cited by 1
- NumberField.mixedEmbedding.norm_eq_zero_iff'proof · cited by 1
- LinearMap.ortho_smul_leftproof · cited by 0
- RCLike.normSq_eq_zeroproof · cited by 0
- groupCohomology.exists_mul_galRestrict_of_norm_eq_oneproof · cited by 0
- LinearMap.linearIndependent_of_isOrthoᵢproof · cited by 0