Commit 2026-02-04 15:37 1b829191

View on Github →

chore(UpperHalfPlane): redefine as a structure (#34597) Make UpperHalfPlane into a two-field structure rather than a type alias for a subtype, to reduce defeq abuse.

Estimated changes

modified def UpperHalfPlane.I
added theorem UpperHalfPlane.coe_inj
deleted theorem UpperHalfPlane.ext'
deleted theorem UpperHalfPlane.ext
deleted theorem UpperHalfPlane.ext_iff'
modified theorem UpperHalfPlane.im_pos
deleted def UpperHalfPlane.mk
deleted theorem UpperHalfPlane.ne_int
deleted theorem UpperHalfPlane.ne_nat
added structure UpperHalfPlane
deleted def UpperHalfPlane
modified theorem UpperHalfPlane.center_zero