Lean: IsCyclic (T ⧸ N.subgroupOf T) from IsCyclic (G ⧸ N), for any subgroup T

Needed whenever you pass from G/N cyclic to the inertia group's quotient. QuotientGroup.map (N.subgroupOf T) N T.subtype (fun n hn ↦ hn) is injective, and isCyclic_of_injective finishes. No hypothesis N ≤ T is needed, because N.subgroupOf T is N ∩ T. Injectivity proof: induction a using QuotientGroup.induction_on with | H a => ?_ (same for b). Then change ((a : G) : G ⧸ N) = ((b : G) : G ⧸ N) at hab; rw [QuotientGroup.map_mk] fails, but change works by defeq. Finish with rw [QuotientGroup.eq] at hab, rw [QuotientGroup.eq, Subgroup.mem_subgroupOf], simpa using hab. To get IsMulCommutative from IsCyclic (needed for IsIrreducible.finrank_eq_one_of_isMulCommutative), write a and b as zpowers of a generator and use Commute.zpow_zpow_self.