Mathlib Map

Theorems · Inductive type · group theory

Subgroup.Characteristic

{G : Type u_1} → [inst : Group G] → Subgroup G → Prop

A subgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

Defined in
Mathlib.Algebra.Group.Subgroup.Basic
Cited by
20 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Subgroup.upperCentralSeries_one · cited by 7Subgroup.upperCentralSeri…Subgroup.characteristic_iff_comap_eq · cited by 4Subgroup.characteristic_i…Subgroup.upperCentralSeriesAux · cited by 4Subgroup.upperCentralSeri…MulAut.characteristic · cited by 2MulAut.characteristicalternatingGroup.characteristic_kleinFour · cited by 1alternatingGroup.characte…alternatingGroup.normal_kleinFour · cited by 1alternatingGroup.normal_k…Subgroup.characteristic_iff_comap_le · cited by 1Subgroup.characteristic_i…Subgroup.characteristic_iff_le_comap · cited by 1Subgroup.characteristic_i…Subgroup.characteristic_iff_map_eq · cited by 1Subgroup.characteristic_i…Subgroup.Characteristic.fixed · cited by 1Characteristic.fixedupperCentralSeriesAux · cited by 0upperCentralSeriesAuxSubgroup.upperCentralSeries.eq_def · cited by 0upperCentralSeries.eq_defSubgroup.characteristic_biInf · cited by 0Subgroup.characteristic_b…Subgroup.characteristic_biSup · cited by 0Subgroup.characteristic_b…Subgroup.upperCentralSeriesAux.eq_def · cited by 0upperCentralSeriesAux.eq_…Group · cited by 6238GroupSubgroup · cited by 3593SubgroupSubgroup.CharacteristicCITED BYCITES

Cites2

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

  • Groupstatement · cited by 6,238
  • Subgroupstatement · cited by 3,593

Cited by25

Results whose statement or proof uses this declaration.