WikiLeanRecent changes · Flags · Stats · About

Diff — Circle

Revision #1871 → #1883 · back to history

modifiedPerpendicular to radius at endpoint is tangent5721baaa9dbd
FieldFrom #1871To #1883
mathlib.declEuclideanGeometry.IsTangentAt_of_angle_eq_pi_div_twoEuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two