Theorem Archimedean.embedReal_apply

Modification history

2025-12-16 09:51
Mathlib/Data/Real/Embedding.lean
chore(Data): fix whitespace (#32931)
Modified Archimedean.embedReal_applyView on Github →
2025-07-24 12:57
Mathlib/Data/Real/Embedding.lean
feat(Data/Real): add embedding of archimedean groups into Real (#26114) …
Added Archimedean.embedReal_applyView on Github →