# 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.