Theorems · Theorem
Nontrivial.exists_pair_ne
∀ {α : Type u_3} [self : Nontrivial α], ∃ x y, x ≠ yIn a nontrivial type, there exists a pair of distinct terms.
- Defined in
- Mathlib.Logic.Nontrivial.Defs
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- Nontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by12
Results whose statement or proof uses this declaration.
- exists_pair_neproof · cited by 32
- nontrivial_iffproof · cited by 12
- Module.Basis.index_nonemptyproof · cited by 10
- Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flatproof · cited by 4
- AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReducedproof · cited by 3
- IsLocalHom.isFieldproof · cited by 2
- Semifield.toIsFieldproof · cited by 1
- Ideal.Quotient.isDomain_iff_primeproof · cited by 1
- Subalgebra.isField_of_algebraicproof · cited by 0
- IsField.of_isDomain_of_finiteproof · cited by 0
- PreTilt.isDomainproof · cited by 0
- IsArtinianRing.isField_of_isDomainproof · cited by 0