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.