Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finite_dimensional.proper_is_R_or_C

Modification history

2023-01-24 03:14
src/data/is_R_or_C/basic.lean
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217) …
Modified finite_dimensional.proper_is_R_or_CView on Github →
2021-12-08 22:28
src/data/complex/is_R_or_C.lean
refactor(data/complex/is_R_or_C): `finite_dimensional.proper_is_R_or_C` is not an `instance` anymore (#10629) …
Added finite_dimensional.proper_is_R_or_CView on Github →