Theorems · Theorem · group theory
sub_ne_zero_of_ne
∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a ≠ b → a - b ≠ 0- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- SubtractionMonoid
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.
- SubtractionMonoidstatement and proof · cited by 208
- eq_of_sub_eq_zeroproof · cited by 27
Cited by51
Results whose statement or proof uses this declaration.
- Complex.canonicalFactor_ne_zeroproof · cited by 6
- MeromorphicAt.derivproof · cited by 6
- WeierstrassCurve.Affine.nonsingular_negAddproof · cited by 4
- WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne'proof · cited by 3
- linearIndependent_monoidHomproof · cited by 3
- Polynomial.pairwise_coprime_X_sub_Cproof · cited by 3
- Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eqproof · cited by 3
- Sbtw.sOppSide_of_notMem_of_memproof · cited by 3
- LinearIndependent.pair_add_smul_add_smul_iffproof · cited by 3
- natCast_le_analyticOrderAtproof · cited by 2
- IsPrimitiveRoot.geom_sum_eq_zeroproof · cited by 2
- Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_rangeproof · cited by 2