Commit 2024-03-28 18:15 57f72eea
View on Github →feat: add card_eq_NrRealPlaces_add_NrComplexPlaces (#11745)
We add card_eq_NrRealPlaces_add_NrComplexPlaces: Fintype.card (InfinitePlace K).card = NrRealPlaces K + NrComplexPlaces K for a number field K.