Theorem Complex.closedEmbedding_intCast

Modification history

2026-04-15 08:53
Mathlib/Analysis/Complex/Basic.lean
feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) (#37601) …
Deleted Complex.closedEmbedding_intCastView on Github →
2024-11-15 10:19
Mathlib/Analysis/Complex/Basic.lean
feat(Analysis): integer complement in `ℂ` (#16542) …
Added Complex.closedEmbedding_intCastView on Github →