Similar.angle_eq_all
∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
[inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
[inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
{a b c : P₁} {a' b' c' : P₂},
Similar ![a, b, c] ![a', b', c'] →
EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' ∧
EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' ∧
EuclideanGeometry.angle c a b = EuclideanGeometry.angle c' a' b'In two similar triangles, all three corresponding angles are equal.
- Defined in
- Mathlib.Geometry.Euclidean.Similarity
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- InnerProductSpacestatement and proof · cited by 3,523
- MetricSpacestatement and proof · cited by 1,684
- NormedAddTorsorstatement and proof · cited by 1,325
- Matrix.vecConsstatement and proof · cited by 852
- Matrix.vecEmptystatement and proof · cited by 832
- EuclideanGeometry.anglestatement · cited by 187
- Similarstatement and proof · cited by 49
- Similar.comm_leftproof · cited by 3
- Similar.comm_rightproof · cited by 2
- Similar.angle_eqproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.