Theoremsbot, card_infinitePlace, id, isUnramified, top, trans, IsUnramifiedAtInfinitePlaces_of_odd_card_aut, IsUnramifiedAtInfinitePlaces_of_odd_finrank, coe_stabilizer_mk, isUnramified_mk_iff, mk_isRamified, mk_isUnramified, exists_comp_symm_eq_of_comp_eq, of_comap, comap_embedding, comap_embedding_conjugate, isComplex, isMixed_conjugate_embedding, isMixed_embedding, isReal, ne_conjugate, comap, isUnramified, comap, comap_algHom, eq, isUnmixed, isUnmixed_conjugate, of_restrictScalars, stabilizer_eq_bot, comap_eq, embedding_comp_eq_or_conjugate_embedding_comp_eq, isComplex_of_isComplex_under, isReal_of_isReal_over, mk_embedding_comp, card_eq_card_isUnramifiedIn, card_isUnramified, card_isUnramified_compl, card_mono, card_stabilizer, comap_apply, comap_comp, comap_embedding_of_isReal, comap_id, comap_mk, comap_mk_lift, comap_smul, comap_surjective, comp_of_comap_eq, even_card_aut_of_not_isUnramified, even_card_aut_of_not_isUnramifiedIn, even_finrank_of_not_isUnramified, even_finrank_of_not_isUnramifiedIn, even_nat_card_aut_of_not_isUnramified, exists_isConj_of_isRamified, exists_smul_eq_of_comap_eq, isComplex_smul_iff, isRamified_iff, isRamified_iff_card_stabilizer_eq_two, isRamified_mk_iff_isMixed, isReal_comap_iff, isReal_smul_iff, isUnramified, isUnramifiedIn, isUnramifiedIn_comap, isUnramified_iff, isUnramified_iff_card_stabilizer_eq_one, isUnramified_iff_mult_le, isUnramified_iff_stabilizer_eq_bot, isUnramified_mk_iff_forall_isConj, isUnramified_mk_iff_isUnmixed, isUnramified_self, isUnramified_smul_iff, mem_orbit_iff, mem_stabilizer_mk_iff, mult_comap_le, nat_card_stabilizer_eq_one_or_two, not_isUnramified_iff, not_isUnramified_iff_card_stabilizer_eq_two, orbitRelEquiv_apply_mk'', smul_apply, smul_coe_apply, smul_eq_comap, smul_mk | 84 |