Statistics

Metric	Count
Definitions `Similar`, `«term_∼_»`	2
Theorems `similar`, `comm_left`, `comm_right`, `comp_isometry_left`, `comp_isometry_left_iff`, `comp_isometry_right`, `comp_isometry_right_iff`, `comp_left`, `comp_left_iff`, `comp_right`, `comp_right_iff`, `exists_dist_eq`, `exists_edist_eq`, `exists_nndist_eq`, `exists_pairwise_dist_eq`, `exists_pairwise_edist_eq`, `exists_pairwise_nndist_eq`, `exists_pos_dist_eq`, `exists_pos_pairwise_dist_eq`, `index_equiv`, `index_map`, `of_exists_dist_eq`, `of_exists_edist_eq`, `of_exists_nndist_eq`, `of_exists_pairwise_dist_eq`, `of_exists_pairwise_edist_eq`, `of_exists_pairwise_nndist_eq`, `of_exists_pos_dist_eq`, `of_exists_pos_pairwise_dist_eq`, `of_subsingleton_index`, `refl`, `reverse_of_three`, `trans`, `similar_comm`, `similar_iff_exists_dist_eq`, `similar_iff_exists_edist_eq`, `similar_iff_exists_nndist_eq`, `similar_iff_exists_pairwise_dist_eq`, `similar_iff_exists_pairwise_edist_eq`, `similar_iff_exists_pairwise_nndist_eq`, `similar_iff_exists_pos_dist_eq`, `similar_iff_exists_pos_pairwise_dist_eq`, `similar_of_dist_mul_eq_dist_mul_eq`, `similar_of_side_side`	44
Total	46

Congruent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`similar` 📖	mathematical	`Congruent`	`Similar`	—	`one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `one_mul`

Similar

Definitions

Name	Category	Theorems
`«term_∼_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm_left` 📖	—	`Similar` `Matrix.vecCons` `Matrix.vecEmpty`	—	—	`Fintype.complete` `Equiv.swap_apply_left` `Equiv.swap_apply_right` `Equiv.swap_apply_of_ne_of_ne`
`comm_right` 📖	—	`Similar` `Matrix.vecCons` `Matrix.vecEmpty`	—	—	`Fintype.complete` `Equiv.swap_apply_of_ne_of_ne` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Equiv.swap_apply_left` `Equiv.swap_apply_right`
`comp_isometry_left` 📖	—	`Isometry` `Similar`	—	—	`comp_left` `Dilation.toDilationClass`
`comp_isometry_left_iff` 📖	mathematical	`Isometry`	`Similar`	—	`comp_left_iff` `Dilation.toDilationClass`
`comp_isometry_right` 📖	—	`Isometry` `Similar`	—	—	`comp_right` `Dilation.toDilationClass`
`comp_isometry_right_iff` 📖	mathematical	`Isometry`	`Similar`	—	`comp_right_iff` `Dilation.toDilationClass`
`comp_left` 📖	mathematical	`Similar`	`DFunLike.coe`	—	`trans` `Dilation.ratio_ne_zero` `Dilation.edist_eq`
`comp_left_iff` 📖	mathematical	—	`Similar` `DFunLike.coe`	—	`trans` `comp_right` `refl` `comp_left`
`comp_right` 📖	mathematical	`Similar`	`DFunLike.coe`	—	`symm` `comp_left`
`comp_right_iff` 📖	mathematical	—	`Similar` `DFunLike.coe`	—	`similar_comm` `comp_left_iff`
`exists_dist_eq` 📖	mathematical	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	`Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instMul` `NNReal.toReal`	—	`similar_iff_exists_dist_eq`
`exists_edist_eq` 📖	mathematical	`Similar`	`EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`similar_iff_exists_edist_eq`
`exists_nndist_eq` 📖	mathematical	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`similar_iff_exists_nndist_eq`
`exists_pairwise_dist_eq` 📖	mathematical	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	`Pairwise` `Real` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`similar_iff_exists_pairwise_dist_eq`
`exists_pairwise_edist_eq` 📖	mathematical	`Similar`	`Pairwise` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`similar_iff_exists_pairwise_edist_eq`
`exists_pairwise_nndist_eq` 📖	mathematical	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	`Pairwise` `NNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`similar_iff_exists_pairwise_nndist_eq`
`exists_pos_dist_eq` 📖	mathematical	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	—	`similar_iff_exists_pos_dist_eq`
`exists_pos_pairwise_dist_eq` 📖	mathematical	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLT` `Real.instZero` `Pairwise` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	—	`similar_iff_exists_pos_pairwise_dist_eq`
`index_equiv` 📖	mathematical	—	`Similar` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.apply_symm_apply` `index_map`
`index_map` 📖	—	`Similar`	—	—	—
`of_exists_dist_eq` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instMul` `NNReal.toReal`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`similar_iff_exists_dist_eq`
`of_exists_edist_eq` 📖	mathematical	`EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	`Similar`	—	`similar_iff_exists_edist_eq`
`of_exists_nndist_eq` 📖	mathematical	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`similar_iff_exists_nndist_eq`
`of_exists_pairwise_dist_eq` 📖	mathematical	`Pairwise` `Real` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`similar_iff_exists_pairwise_dist_eq`
`of_exists_pairwise_edist_eq` 📖	mathematical	`Pairwise` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	`Similar`	—	`similar_iff_exists_pairwise_edist_eq`
`of_exists_pairwise_nndist_eq` 📖	mathematical	`Pairwise` `NNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`similar_iff_exists_pairwise_nndist_eq`
`of_exists_pos_dist_eq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`similar_iff_exists_pos_dist_eq`
`of_exists_pos_pairwise_dist_eq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Pairwise` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`similar_iff_exists_pos_pairwise_dist_eq`
`of_subsingleton_index` 📖	mathematical	—	`Similar`	—	`Congruent.similar` `Congruent.of_subsingleton_index`
`refl` 📖	mathematical	—	`Similar`	—	`one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `Nat.cast_one` `one_mul`
`reverse_of_three` 📖	—	`Similar` `Matrix.vecCons` `Matrix.vecEmpty`	—	—	`comm_left` `comm_right`
`trans` 📖	—	`Similar`	—	—	`mul_ne_zero` `NNReal.instNoZeroDivisors` `ENNReal.coe_mul` `mul_assoc`

(root)

Definitions

Name	Category	Theorems
`Similar` 📖	MathDef	29 math math: `Similar.of_exists_edist_eq`, `similar_iff_exists_dist_eq`, `similar_iff_exists_nndist_eq`, `similar_iff_exists_edist_eq`, `similar_comm`, `Similar.comp_right_iff`, `similar_iff_exists_pairwise_dist_eq`, `Similar.of_exists_pos_dist_eq`, `similar_of_side_side`, `Similar.comp_isometry_left_iff`, `similar_iff_exists_pairwise_edist_eq`, `Similar.comp_left_iff`, `EuclideanGeometry.similar_of_side_angle_side`, `Similar.of_exists_pos_pairwise_dist_eq`, `similar_iff_exists_pairwise_nndist_eq`, `EuclideanGeometry.similar_of_angle_angle`, `Similar.of_exists_pairwise_dist_eq`, `Similar.index_equiv`, `Similar.of_exists_pairwise_nndist_eq`, `similar_of_dist_mul_eq_dist_mul_eq`, `Congruent.similar`, `similar_iff_exists_pos_pairwise_dist_eq`, `Similar.of_exists_pairwise_edist_eq`, `Similar.of_exists_dist_eq`, `Similar.comp_isometry_right_iff`, `Similar.of_exists_nndist_eq`, `Similar.of_subsingleton_index`, `similar_iff_exists_pos_dist_eq`, `Similar.refl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`similar_comm` 📖	mathematical	—	`Similar`	—	`Similar.symm`
`similar_iff_exists_dist_eq` 📖	mathematical	—	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instMul` `NNReal.toReal`	—	`similar_iff_exists_nndist_eq` `dist_nndist`
`similar_iff_exists_edist_eq` 📖	mathematical	—	`Similar` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	—
`similar_iff_exists_nndist_eq` 📖	mathematical	—	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`edist_nndist`
`similar_iff_exists_pairwise_dist_eq` 📖	mathematical	—	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Pairwise` `Real` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`Nat.cast_zero`
`similar_iff_exists_pairwise_edist_eq` 📖	mathematical	—	`Similar` `Pairwise` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`similar_iff_exists_edist_eq` `PseudoEMetricSpace.edist_self` `MulZeroClass.mul_zero`
`similar_iff_exists_pairwise_nndist_eq` 📖	mathematical	—	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Pairwise` `NNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`edist_nndist` `Nat.cast_zero`
`similar_iff_exists_pos_dist_eq` 📖	mathematical	—	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	—	`similar_iff_exists_dist_eq` `NNReal.instCanonicallyOrderedAdd`
`similar_iff_exists_pos_pairwise_dist_eq` 📖	mathematical	—	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLT` `Real.instZero` `Pairwise` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	—	`NNReal.instCanonicallyOrderedAdd`
`similar_of_dist_mul_eq_dist_mul_eq` 📖	mathematical	`Real` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Matrix.vecCons` `Matrix.vecEmpty`	—	`div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_le_of_ne'` `dist_nonneg` `Similar.of_exists_pos_pairwise_dist_eq` `Fintype.complete` `dist_self` `MulZeroClass.mul_zero`
`similar_of_side_side` 📖	mathematical	`Real` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist`	`Similar` `PseudoMetricSpace.toPseudoEMetricSpace` `Matrix.vecCons` `Matrix.vecEmpty`	—	`similar_of_dist_mul_eq_dist_mul_eq`

---

← Back to Index

Documentation Verification Report

Similarity

Statistics

Congruent

Theorems

Similar

Definitions

Theorems

(root)

Definitions

Theorems