Theorem ContinuousAlgEquiv.surjective

Modification history

2025-12-19 16:47

Mathlib/Topology/Algebra/Algebra/Equiv.lean

feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` (#30576)

Added ContinuousAlgEquiv.surjective View on Github →