Commit 2023-05-18 22:00 83a66c87

View on Github →

chore(measure_theory/special_functions/basic): split (#19040) Split out the facts about is_R_or_C from measure_theory/function/special_functions/basic (a foundational file, imported by the Bochner integral construction). These facts are heavier-weight than one would expect because the fact that an is_R_or_C field is a proper space currently passes through the corresponding fact for a general finite-dimensional normed space.

Estimated changes