Theorem NumberField.InfinitePlace.isometry_embedding_of_isReal

Modification history

2025-11-28 16:39
Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean
refactor: use isometry extensions for completions at infinite places of number fields (#29969) …
Added NumberField.InfinitePlace.isometry_embedding_of_isRealView on Github →