Mathlib Map

Theorems · Definition · group theory

Equiv.subRight

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

A version of Equiv.addRight (-a) b that is defeq to b - a.

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

Around this declaration

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

Homeomorph.subRight · cited by 9Homeomorph.subRightnhds_eq_iInf_abs_sub · cited by 5nhds_eq_iInf_abs_subOrderIso.subRight · cited by 4OrderIso.subRightEquiv.subRight_apply · cited by 4Equiv.subRight_applyIsometryEquiv.subRight · cited by 3IsometryEquiv.subRightMeasurableEquiv.subRight · cited by 2MeasurableEquiv.subRightValuation.isEquiv_iff_val_sub_one_lt_one · cited by 2Valuation.isEquiv_iff_val…Meromorphic.meromorphic_comp_add_const_iff_meromorphic · cited by 2Meromorphic.meromorphic_c…MeasurableEquiv.shearSubRight · cited by 1MeasurableEquiv.shearSubR…Matrix.circulant_mul · cited by 1Matrix.circulant_muljacobiTheta₂'_add_left' · cited by 1jacobiTheta₂'_add_left'Equiv.subRight_eq_addRight_neg · cited by 0Equiv.subRight_eq_addRigh…Equiv.subRight_symm_apply · cited by 0Equiv.subRight_symm_applysum_translate · cited by 0sum_translateIsometryEquiv.subRight_toEquiv · cited by 0IsometryEquiv.subRight_to…Equiv · cited by 8337EquivAddGroup · cited by 4410AddGroupEquiv.subRightCITED 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
  • AddGroupstatement and proof · cited by 4,410

Cited by15

Results whose statement or proof uses this declaration.