median_to_hypotenuse

Mathlib.Geometry.RightTriangle

Packages

Module

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Statement

forall (Midpoint : forall (M : Vec), forall (B : Vec), forall (C : Vec), Prop), forall (M : Vec), forall (A : Vec), forall (B : Vec), forall (C : Vec), forall (h : RightTriangle A B C), forall (hm : Midpoint M B C), @Eq.{1} RingElem (distSq A M) (distSq B M)

Proof term

fun Midpoint => fun M => fun A => fun B => fun C => fun h => fun hm => @Eq.refl.{1} RingElem (distSq A M)

Constants

Mathlib.Algebra.Ring.RingElem

Interface hash: sha256:29d995d6a38e44a010f577d64428b3272226781f7982e2306784cb3bdc4977ea

Mathlib.Geometry.RightTriangle.RightTriangle

Interface hash: sha256:6f588334640ef184d8be6fbdf69285b0e8c0c5af216cf2e3c9df77e058eded9b

Mathlib.Vector.Basic.Vec

Interface hash: sha256:bc9e713ccaaae78bf5ef428fe3455d47b8f8432e58b79a82bf806866b713e287

Mathlib.Vector.Dot.distSq

Interface hash: sha256:5ac54f1e61b75c804955d1e59695207380bedc448b775db4267dfa4c1feaf8ad

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015