Mathlib Map

Theorems · Theorem · general topology

dist_mul_left

∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Mul M] [IsIsometricSMul M M] (a b c : M),
  dist (a * b) (a * c) = dist b c
Defined in
Mathlib.Topology.MetricSpace.IsometricSMul
Cited by
5 results in Mathlib
Foundations
Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PseudoMetricSpaceMulIsIsometricSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

dist_mul_mul_le · cited by 3dist_mul_mul_ledist_self_mul_right · cited by 2dist_self_mul_rightabs_dist_sub_le_dist_mul_mul · cited by 1abs_dist_sub_le_dist_mul_…dist_mul_self_right · cited by 1dist_mul_self_rightdist_div_left · cited by 0dist_div_leftReal · cited by 25697RealPseudoMetricSpace · cited by 1550PseudoMetricSpaceDist.dist · cited by 1539Dist.distIsIsometricSMul · cited by 74IsIsometricSMuldist_smul · cited by 2dist_smuldist_mul_leftCITED BYCITES

Cites5

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

Cited by5

Results whose statement or proof uses this declaration.