← all areas

Namespace IsGalois 6 theorems

• Existence of a p-group layer of index prime to p IsGalois.exists_intermediateField_isPGroup_and_not_dvd_finrank 0 below · cited by 1 · depth 19
• Cyclic p-power quotient of a subgroup of (ℤ/p^k)^× IsGalois.exists_subgroup_fixedField_isCyclic_isPGroup_of_injective_monoidHom_zmod_units 0 below · cited by 1 · depth 23
• Degree-two inflation–restriction for Galois unit groups IsGalois.map_two_units_injective_and_exists_of_map_subtype_eq_zero 4 below · cited by 1 · depth 23
• Galois descent for unit groups, as representations IsGalois.exists_units_quotientToInvariants_iso_res_apply_eq 0 below · cited by 1 · depth 24
• Galois base change along a bijective tensor product map IsGalois.of_bijective_tensorProduct_lift 0 below · cited by 1 · depth 26
• Speiser's theorem: invariant L-basis for semilinear Galois actions IsGalois.exists_basis_baseChange_forall_apply_eq_self 0 below · cited by 1 · depth 27