Mathlib Map

Theorems · Theorem · group theory

mul_mul_div_cancel

∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), a * c * (b / c) = a * b
Defined in
Mathlib.Algebra.Group.Basic
Cited by
1 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext
Assumes
CommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

mabs_mul_eq_oneLePart_sq · cited by 1mabs_mul_eq_oneLePart_sqmul_assoc · cited by 1667mul_assocCommGroup · cited by 990CommGroupmul_div_cancel · cited by 9mul_div_cancelmul_mul_div_cancelCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.