Congruence

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

Statistics

Metric	Count
Definitions	0
Theorems angle_angle_side, angle_eq_of_congruent, angle_side_angle, side_angle_side, side_side_side, triangle_congruent_iff_dist_eq	6
Total	6

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_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 Dist.dist PseudoMetricSpace.toDist	Congruent EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Matrix.vecCons Matrix.vecEmpty	—	angle_add_angle_add_angle_eq_pi ne₁₃_of_not_collinear Set.pair_comm Set.insert_comm angle_side_angle angle_comm AddRightCancelSemigroup.toIsRightCancelAdd Congruent.dist_eq
angle_eq_of_congruent 📖	mathematical	Congruent EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace	angle	—	Nat.instAtLeastTwoHAddOfNat real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two vsub_sub_vsub_cancel_right Congruent.dist_eq
angle_side_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 Dist.dist PseudoMetricSpace.toDist	Congruent EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Matrix.vecCons Matrix.vecEmpty	—	angle_add_angle_add_angle_eq_pi ne₁₃_of_not_collinear Set.insert_comm dist_comm dist_eq_dist_mul_sin_angle_div_sin_angle angle_comm AddRightCancelSemigroup.toIsRightCancelAdd side_angle_side
side_angle_side 📖	mathematical	angle Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	Congruent EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Matrix.vecCons Matrix.vecEmpty	—	side_side_side dist_comm sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_nonneg pow_two Nat.instAtLeastTwoHAddOfNat law_cos
side_side_side 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	Congruent EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Matrix.vecCons Matrix.vecEmpty	—	triangle_congruent_iff_dist_eq Fintype.complete dist_self dist_comm
triangle_congruent_iff_dist_eq 📖	mathematical	—	Congruent EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	congruent_iff_dist_eq

---

← Back to Index