Theorem Equiv.toEmbedding_injective

Modification history

2026-03-24 04:38

Mathlib/Logic/Embedding/Basic.lean

fix: mark projections `@[reducible]` around `RelIso` (#37032) …

Modified Equiv.toEmbedding_injective View on Github →

2024-01-12 06:00

Mathlib/Logic/Embedding/Basic.lean

feat(Cardinal): `#(α ≃ β)` and `#(α ↪ β)` in the infinite case (#9646) …

Added Equiv.toEmbedding_injective View on Github →