Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subalgebra.separates_points.is_R_or_C_to_real

Modification history