ClassFormation.normTopology_norm_continuous
The norm from a finite extension is continuous for the norm topologies of its source and target (continuity of norms).
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]Lean source · statement
theorem normTopology_norm_continuous
(A : Rep ℤ G) (K L : ClosedSubgroup G)
(hLK : L.toSubgroup ≤ K.toSubgroup)
[hLKfinite : Finite
(K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
IsNormContinuous A L K (relativeNorm A K L hLK)