subgroup of prime index

Stream: Is there code for X?

[Edison Xie]

Do we have that a subgroup of minimal prime index dividing the order of the group is normal?

[Edison Xie]

nvm I found Subgroup.normal_of_index_eq_minFac_card but how do I resolve topic, is it not allowed anymore?

[Ruben Van de Velde]

That's correct