Theorem num_smul_one_lt_den_smul_add

Modification history

2025-07-24 12:57
Mathlib/Data/Real/Embedding.lean
feat(Data/Real): add embedding of archimedean groups into Real (#26114) …
Added num_smul_one_lt_den_smul_addView on Github →