Theorem Continuous.of_coeHom_comp

Modification history

2025-04-06 18:39
Mathlib/Topology/Algebra/Group/Basic.lean
feat(NumberTheory): p-adic cyclotomic character (#21934)
Added Continuous.of_coeHom_compView on Github →