Theorem Real.ofDigits_const_last_eq_one

Modification history

2025-11-25 09:05
Mathlib/Analysis/Real/OfDigits.lean
chore: use Fin.last in ofDigits_const_last_eq_one (#32071) …
Modified Real.ofDigits_const_last_eq_oneView on Github →
2025-11-16 18:46
Mathlib/Analysis/Real/OfDigits.lean
feat(Topology): every compact metric space is image of Cantor set (#26184) …
Added Real.ofDigits_const_last_eq_oneView on Github →