Theorems · Theorem · group theory
mul_div
∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
- Assumes
- DivInvMonoid
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.
- mul_assocproof · cited by 1,667
- div_eq_mul_invproof · cited by 715
- DivInvMonoidstatement and proof · cited by 103
Cited by31
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eqproof · cited by 4
- InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zeroproof · cited by 4
- WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eqproof · cited by 4
- catalan_eq_centralBinom_divproof · cited by 3
- SimpleGraph.antitoneOn_extremalNumber_div_choose_twoproof · cited by 3
- Ideal.IsFractionRing.normalproof · cited by 3
- hasSum_one_div_nat_pow_mul_cosproof · cited by 2
- hasSum_one_div_nat_pow_mul_sinproof · cited by 2
- AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_selfproof · cited by 2
- ValuationRing.iff_isInteger_or_isIntegerproof · cited by 2
- AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFnproof · cited by 1
- AkraBazziRecurrence.rpow_p_mul_one_add_smoothingFn_geproof · cited by 1