Theorems · Theorem · group theory

Group.isSolvable_of_ker_le_range

∀ {G : Type u_1} [inst : Group G] {G' : Type u_3} {G'' : Type u_4} [inst_1 : Group G'] [inst_2 : Group G'']
  (f : G' →* G) (g : G →* G''),
  g.ker ≤ f.range → ∀ [hG' : Group.IsSolvable G'] [hG'' : Group.IsSolvable G''], Group.IsSolvable G

Defined in: Mathlib.GroupTheory.Solvable
Cited by: 5 results in Mathlib
Foundations: Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group Group Group Group.IsSolvable Group.IsSolvable

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Groupstatement and proof · cited by 6,238
Bot.botproof · cited by 4,720
MonoidHomstatement and proof · cited by 3,629
Subgroupstatement · cited by 3,593
LE.le.transproof · cited by 3,151
Eq.leproof · cited by 605
MonoidHom.rangestatement and proof · cited by 314
Subgroup.mapproof · cited by 301
MonoidHom.kerstatement and proof · cited by 212
le_bot_iffproof · cited by 116
Group.IsSolvablestatement and proof · cited by 46
MonoidHom.range_eq_mapproof · cited by 37

Cited by5

Results whose statement or proof uses this declaration.

Group.isSolvable_of_isSolvable_injectiveproof · cited by 4
Group.isSolvable_of_surjectiveproof · cited by 4
isSolvable_of_isScalarTowerproof · cited by 1
Group.isSolvable_iff_subgroup_quotientproof · cited by 0
solvable_of_ker_le_rangeproof · cited by 0