embedding_inclusion → IsEmbedding.inclusion
embedding_inclusion is now IsEmbedding.inclusion: Mathlib deprecated on 2024-10-26 (first seen in v4.13.0).
Mathlib removed the deprecated alias in v4.22.0, so code that still uses it fails to compile from that release on.
- Old name
- embedding_inclusion
- Use instead
- IsEmbedding.inclusion
- Module
- Mathlib.Topology.Constructions
- Deprecated
- 2024-10-26 (v4.13.0)
- Alias removed
- v4.22.0
- Type changed?
- not checked in this map: confirm with lake build
- Answer from
- Mathlib's @[deprecated] attribute (confidence 1), source in Mathlib v4.21.0
Look up another
The map holds 17,917 deprecated Mathlib names across v4.0.0 to v4.35.0 (Mathlib commit 56a005855e). On the 145 raw build errors in the 7 pilot projects, the alias map alone resolved 0: most breakage after a bump is a changed signature or a reproof, which is why the benchmark lists the repairs.
Check a whole project at once: scan a GitHub repository.