Def Archimedean.embedReal

Modification history

2025-07-24 12:57

Mathlib/Data/Real/Embedding.lean

feat(Data/Real): add embedding of archimedean groups into Real (#26114) …

Added Archimedean.embedReal View on Github →