Theorems · Theorem · group theory
Group.isSolvable_of_isSolvable_injective
∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
Function.Injective ⇑f → ∀ [Group.IsSolvable G'], Group.IsSolvable G- Defined in
- Mathlib.GroupTheory.Solvable
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupGroupGroup.IsSolvable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Groupstatement and proof · cited by 6,238
- MonoidHomstatement and proof · cited by 3,629
- bot_leproof · cited by 306
- Group.IsSolvablestatement and proof · cited by 46
- MonoidHom.ker_eq_botproof · cited by 10
- Group.isSolvable_of_ker_le_rangeproof · cited by 5
Cited by4
Results whose statement or proof uses this declaration.
- Equiv.Perm.not_isSolvableproof · cited by 1
- gal_isSolvable_towerproof · cited by 1
- gal_mul_isSolvableproof · cited by 1
- solvable_of_solvable_injectiveproof · cited by 0