Yamaguchi26AbfaithfulGalois.formalHilbert90_comp_continuousMulEquiv
Transport actual finite cocycles along each induced open-subgroup isomorphism.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G' : Type v} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G']Lean source · statement
theorem formalHilbert90_comp_continuousMulEquiv
(θ : Orientation p G') (e : G ≃ₜ* G') (hθ : FormalHilbert90 θ) :
FormalHilbert90 (θ.comp (e : G →ₜ* G'))