Commit 2025-08-18 08:28 bb6d4587

View on Github →

chore(Algebra): final batch of Algebra porting notes processing (#28478) This PR finishes going through porting notes in the Algebra folder. A lot of them no longer apply or are wontfixes.

Estimated changes

deleted theorem QuaternionAlgebra.add_imI
deleted theorem QuaternionAlgebra.add_imJ
deleted theorem QuaternionAlgebra.add_imK
deleted theorem QuaternionAlgebra.add_re
deleted theorem QuaternionAlgebra.mul_imI
deleted theorem QuaternionAlgebra.mul_imJ
deleted theorem QuaternionAlgebra.mul_imK
deleted theorem QuaternionAlgebra.mul_re
deleted theorem QuaternionAlgebra.neg_imI
deleted theorem QuaternionAlgebra.neg_imJ
deleted theorem QuaternionAlgebra.neg_imK
deleted theorem QuaternionAlgebra.neg_re
deleted theorem QuaternionAlgebra.one_imI
deleted theorem QuaternionAlgebra.one_imJ
deleted theorem QuaternionAlgebra.one_imK
deleted theorem QuaternionAlgebra.one_re
deleted theorem QuaternionAlgebra.smul_re
deleted theorem QuaternionAlgebra.sub_imI
deleted theorem QuaternionAlgebra.sub_imJ
deleted theorem QuaternionAlgebra.sub_imK
deleted theorem QuaternionAlgebra.sub_re
deleted theorem QuaternionAlgebra.zero_re