Theorems · Theorem · logic and foundations
Eq.trans_ne
∀ {α : Sort u_1} {a b c : α}, a = b → b ≠ c → a ≠ cAlias of ne_of_eq_of_ne.
- Defined in
- Mathlib.Logic.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
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.
- ne_of_eq_of_neproof · cited by 23
Cited by10
Results whose statement or proof uses this declaration.
- MeasureTheory.ae_measure_preimage_add_right_lt_topproof · cited by 1
- AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree'proof · cited by 1
- MeasureTheory.ae_measure_preimage_mul_right_lt_topproof · cited by 1
- ZetaAsymptotics.tendsto_Gamma_term_auxproof · cited by 1
- PrimeSpectrum.exist_ltSeries_mem_one_of_mem_lastproof · cited by 1
- Polynomial.Sequence.linearIndependentproof · cited by 1
- exists_right_inv_of_exists_left_invproof · cited by 1
- Ordinal.invVeblen₁_eq_iffproof · cited by 1
- jacobiSum_mul_jacobiSum_invproof · cited by 0
- JacobsonNoether.exists_separable_and_not_isCentral'proof · cited by 0