Theorems · Theorem · group theory
div_eq_div_iff
∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → d ≠ 0 → (a / b = c / d ↔ a * d = c * b)- Cited by
- 22 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommGroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ne.isUnitproof · cited by 99
- CommGroupWithZerostatement and proof · cited by 94
- IsUnit.div_eq_div_iffproof · cited by 3
Cited by22
Results whose statement or proof uses this declaration.
- RatFunc.num_div_denomproof · cited by 18
- FractionalIdeal.count_well_definedproof · cited by 5
- WeierstrassCurve.Jacobian.X_eq_iffproof · cited by 3
- WeierstrassCurve.Projective.X_eq_iffproof · cited by 3
- Liouville.irrationalproof · cited by 3
- IsFractionRing.isInvariant_of_isIntegralproof · cited by 2
- ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRelproof · cited by 2
- WeierstrassCurve.Jacobian.Y_eq_iff'proof · cited by 1
- NNRat.cast_injectiveproof · cited by 1
- Real.Wallis.W_eq_factorial_ratioproof · cited by 1
- WeierstrassCurve.Projective.Y_eq_iff'proof · cited by 1
- FractionalIdeal.absNorm_div_norm_eq_absNorm_div_normproof · cited by 1