Theorems · Theorem · group theory
div_eq_one_iff_eq
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, b ≠ 0 → (a / b = 1 ↔ a = b)- Cited by
- 16 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
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.
- GroupWithZerostatement and proof · cited by 691
- Ne.isUnitproof · cited by 99
- IsUnit.div_eq_one_iff_eqproof · cited by 1
Cited by16
Results whose statement or proof uses this declaration.
- strictConcaveOn_log_Ioiproof · cited by 5
- Real.smoothTransition.one_of_one_leproof · cited by 3
- ValuationRing.iff_isInteger_or_isIntegerproof · cited by 2
- exists_contMDiff_support_eq_eq_one_iffproof · cited by 2
- BoundedContinuousFunction.ext_of_char_eqproof · cited by 1
- Rel.edgeDensity_add_edgeDensity_complproof · cited by 1
- maximalIdeal_isPrincipal_of_isDedekindDomainproof · cited by 1
- tendsto_div_nhds_one_iff_eq₀proof · cited by 1
- Complex.exp_eq_exp_iff_exp_sub_eq_oneproof · cited by 1
- ProbabilityTheory.lintegral_betaPDF_eq_oneproof · cited by 1
- commProb_eq_one_iffproof · cited by 1
- IsPreconnected.eq_or_eq_neg_of_sq_eqproof · cited by 1