Mathlib Map

Theorems · Definition · group theory

Equiv.divRight

{G : Type u_5} → [Group G] → G → G ≃ G

A version of Equiv.mulRight a⁻¹ b that is defeq to b / a.

Defined in
Mathlib.Algebra.Group.Units.Equiv
Cited by
5 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Homeomorph.divRight · cited by 10Homeomorph.divRightnhds_eq_iInf_mabs_div · cited by 5nhds_eq_iInf_mabs_divOrderIso.divRight · cited by 4OrderIso.divRightIsometryEquiv.divRight · cited by 3IsometryEquiv.divRightMeasurableEquiv.divRight · cited by 2MeasurableEquiv.divRightMeasurableEquiv.shearDivRight · cited by 1MeasurableEquiv.shearDivR…Equiv.divRight_apply · cited by 1Equiv.divRight_applyIsometryEquiv.divRight_toEquiv · cited by 0IsometryEquiv.divRight_to…Equiv.divRight_eq_mulRight_inv · cited by 0Equiv.divRight_eq_mulRigh…Equiv.divRight_symm_apply · cited by 0Equiv.divRight_symm_applyEquiv · cited by 8337EquivGroup · cited by 6238GroupEquiv.divRightCITED BYCITES

Cites2

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

  • Equivstatement · cited by 8,337
  • Groupstatement and proof · cited by 6,238

Cited by10

Results whose statement or proof uses this declaration.