Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
ereal.coe_to_real
Modification history
2021-06-18 18:18
src/data/real/ereal.lean
chore(topology/basic): rename compact_Icc to is_compact_Icc (#7979) …
Added
ereal.coe_to_real
View on Github →