Mathlib Map

Theorems · Theorem · general topology

IsometryEquiv.divLeft_symm_apply

∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (c b : G), (IsometryEquiv.divLeft c).symm b = b⁻¹ * c
Defined in
Mathlib.Topology.MetricSpace.IsometricSMul
Cited by
1 results in Mathlib
Foundations
Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
GroupPseudoEMetricSpaceIsIsometricSMulIsIsometricSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

QuotientGroup.norm_mk · cited by 1QuotientGroup.norm_mkDFunLike.coe · cited by 62936DFunLike.coeGroup · cited by 6238GroupPseudoEMetricSpace · cited by 1536PseudoEMetricSpaceMulOpposite · cited by 1135MulOppositeIsometryEquiv · cited by 177IsometryEquivIsometryEquiv.symm · cited by 75IsometryEquiv.symmIsIsometricSMul · cited by 74IsIsometricSMulIsometryEquiv.divLeft · cited by 5IsometryEquiv.divLeftIsometryEquiv.divLeft_symm_ap…CITED BYCITES

Cites8

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.