Documentation

EuclideanGeometry.Foundation.Axiom.Triangle.Similarity_trash

source
theorem EuclidGeom.sim_of_AA' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (h₂ : tr₁.angle₂.dvalue = tr₂.angle₂.dvalue) (h₃ : tr₁.angle₃.value = tr₂.angle₃.value) :
EuclidGeom.HasSim.sim tr₁ tr₂
source
theorem EuclidGeom.sim_of_AA_of_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (h₁ : tr₁.IsRt) (h₂ : tr₂.IsRt) (h : tr₁.angle₂.dvalue = tr₂.angle₂.dvalue) :
EuclidGeom.HasSim.sim tr₁ tr₂
source
theorem EuclidGeom.asim_of_AA' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (h₂ : tr₁.angle₂.dvalue = -tr₂.angle₂.dvalue) (h₃ : tr₁.angle₃.value = -tr₂.angle₃.value) :
EuclidGeom.HasASim.asim tr₁ tr₂
source
theorem EuclidGeom.asim_of_AA_of_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (h₁ : tr₁.IsRt) (h₂ : tr₂.IsRt) (h : tr₁.angle₂.dvalue = -tr₂.angle₂.dvalue) :
EuclidGeom.HasASim.asim tr₁ tr₂