Theorems · Theorem · group theory
eq_div_iff
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (c = a / b ↔ c * b = a)- Cited by
- 38 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.eq_div_iffproof · cited by 3
Cited by38
Results whose statement or proof uses this declaration.
- Real.log_sqrtproof · cited by 5
- Real.HolderConjugate.sub_one_mul_conjproof · cited by 4
- RatFunc.eq_C_of_minpolyX_coeff_eq_zeroproof · cited by 3
- hasSum_zeta_natproof · cited by 3
- ValuativeRel.ValueGroupWithZero.mk_eq_divproof · cited by 3
- RatFunc.num_mul_eq_mul_denom_iffproof · cited by 3
- isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injectiveproof · cited by 2
- hasSum_one_div_nat_pow_mul_fourierproof · cited by 2
- DirichletCharacter.LSeries_twist_vonMangoldt_eqproof · cited by 2
- ValuationRing.iff_isInteger_or_isIntegerproof · cited by 2
- HurwitzZeta.hasSum_int_sinKernelproof · cited by 2