Documentation Verification Report

Similarity

📁 Source: Mathlib/Geometry/Euclidean/Similarity.lean

Statistics

Metric	Count
Definitions	0
Theorems `similar_of_angle_angle`, `similar_of_side_angle_side`, `angle_eq`, `angle_eq_all`	4
Total	4

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`similar_of_angle_angle` 📖	mathematical	`Collinear` `Real` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instInsert` `Set.instSingletonSet` `angle`	`Similar` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Nat.instAtLeastTwoHAddOfNat` `angle_lt_pi_div_two_of_angle_eq_pi_div_two` `ne₂₃_of_not_collinear` `ne₁₂_of_not_collinear` `angle_add_angle_add_angle_eq_pi` `law_sin` `Similar.reverse_of_three` `Similar.comm_left` `similar_of_side_side` `ne_of_gt` `mul_comm` `div_eq_div_iff` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `mul_div_assoc` `eq_div_iff_mul_eq`
`similar_of_side_angle_side` 📖	mathematical	`Collinear` `Real` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instInsert` `Set.instSingletonSet` `angle` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist`	`Similar` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Matrix.vecCons` `Matrix.vecEmpty`	—	`ne₁₂_of_not_collinear` `ne₂₃_of_not_collinear` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `div_eq_div_iff` `Nat.instAtLeastTwoHAddOfNat` `law_cos` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `dist_nonneg` `similar_iff_exists_pos_pairwise_dist_eq` `Fintype.complete` `dist_self` `MulZeroClass.mul_zero` `dist_comm` `pow_left_inj₀` `IsOrderedRing.toMulPosMono` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `mul_pow` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval`

Similar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angle_eq` 📖	mathematical	`Similar` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Matrix.vecCons` `Matrix.vecEmpty`	`EuclideanGeometry.angle`	—	`similar_iff_exists_pos_dist_eq` `Nat.instAtLeastTwoHAddOfNat` `EuclideanGeometry.law_cos` `mul_eq_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `mul_eq_zero_iff_right` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `dist_eq_zero` `EuclideanGeometry.angle_self_left` `EuclideanGeometry.angle_self_right` `Real.injOn_cos` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt`
`angle_eq_all` 📖	mathematical	`Similar` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Matrix.vecCons` `Matrix.vecEmpty`	`EuclideanGeometry.angle`	—	`angle_eq` `comm_right` `comm_left`

---

← Back to Index