Theorems · Theorem
nontrivial_iff
∀ {α : Type u_1}, Nontrivial α ↔ ∃ x y, x ≠ y- Defined in
- Mathlib.Logic.Nontrivial.Defs
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nontrivialstatement and proof · cited by 2,416
- Nontrivial.exists_pair_neproof · cited by 12
Cited by12
Results whose statement or proof uses this declaration.
- ArchimedeanClass.mk_smulproof · cited by 2
- SimpleGraph.preconnected_bot_iff_subsingletonproof · cited by 2
- integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrableproof · cited by 2
- Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_mapproof · cited by 2
- exists_ne_zero_dotProduct_eq_zeroproof · cited by 2
- IsSMulRegular.not_zero_iffproof · cited by 1
- Cardinal.two_le_iffproof · cited by 1
- not_isLeftRegular_zero_iffproof · cited by 1
- not_isRightRegular_zero_iffproof · cited by 1
- Fintype.one_lt_card_iffproof · cited by 0
- normalClosure_of_stabilizer_eq_topproof · cited by 0
- Cardinal.two_le_iff'proof · cited by 0