Theorem NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex_apply

Modification history

2026-04-13 19:44
Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
feat: `NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank` (#30551) …
Added NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex_applyView on Github →