Commit 2025-03-14 05:54 f033aca7

View on Github →

chore(Data): go through remaining porting notes (#22907) This PR goes through all porting notes in Mathlib/Data and reviews them. Most of the notes can simply be applied or dropped.

Estimated changes

modified theorem Complex.conj_neg_I
modified theorem Complex.normSq_div
modified theorem Complex.normSq_inv
modified theorem Complex.normSq_one
modified theorem Complex.normSq_zero
added theorem Cardinal.mk_complex
deleted theorem mk_complex
deleted theorem mk_univ_complex
modified theorem PFun.prodMap_id_id
modified theorem PNat.mk_le_mk
modified theorem PNat.mk_lt_mk
modified theorem PNat.one_le_find
modified theorem Prod.mk_inj