Commit 2025-03-01 13:59 a197b52d

feat(NumberField/InfinitePlaces): add prod_eq_prod_mul_prod (#22380) When dealing with infinite places, it is sometimes necessary to distinguish between real and complex places. For that, we add the result:

theorem prod_eq_prod_mul_prod {α : Type*} [CommMonoid α] [NumberField K] (f : InfinitePlace K → α) :
     ∏ w, f w = (∏ w : {w // IsReal w}, f w.1) * (∏ w : {w // IsComplex w}, f w.1) 

(and the corresponding additive version). Also we add lemmas to simplify mult w when w is of type IsReal or IsComplex. Thanks to these, we can (slightly) golf some proofs.