Commit 2026-03-25 16:54 e899c466

View on Github →

refactor: make Unitization into a one-field structure (#37014) I've been meaning to do this for a while; indeed, I created this branch 2 years ago! The purpose now is to avoid some defeq abuse related to Unitization. In this case, especially since I already had this branch, I decided that the easiest thing to do would be to turn it into a one-field structure. I have removed a few of the IsDefEq.respectTransparency overrides, just to verify that this really solved the problem and that it didn't lie elsewhere. Probably more can be removed elsewhere, but we'll leave those to automation.

Estimated changes

modified def Unitization.addEquiv
deleted theorem Unitization.ext
deleted def Unitization.fst
added theorem Unitization.inl_inj
modified theorem Unitization.inl_neg
modified def Unitization.inrHom
modified theorem Unitization.inr_inj
modified theorem Unitization.inr_neg
modified theorem Unitization.linearMap_ext
added theorem Unitization.mk_toProd
deleted def Unitization.snd
modified def Unitization.sndHom
added theorem Unitization.toProd_add
added theorem Unitization.toProd_mk
added theorem Unitization.toProd_neg
added structure Unitization
deleted def Unitization