Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dense_embedding_id

Modification history

2022-12-07 18:26
src/topology/dense_embedding.lean
feat(topology/algebra/uniform_ring): add dense_inducing.extend_hom (#17212) …
Added dense_embedding_idView on Github →