Theorem Continuous.of_coeHom_comp

Modification history

2026-08-24 07:44
Mathlib/Topology/Algebra/Group/Basic.lean
refactor(Topology/Algebra/Group): split long file Basic.lean (#43010) …
Modified Continuous.of_coeHom_compView on Github →
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 →