Documentation Verification Report

IsSubnormal

📁 Source: Mathlib/GroupTheory/IsSubnormal.lean

Statistics

Metric	Count
Definitions `IsSubnormal`, `IsSubnormal`	2
Theorems `addSubgroupOf`, `bot`, `comap`, `eq_bot_or_top_of_isSimpleAddGroup`, `exists_normal_and_le_and_lt_top_of_ne`, `iff_eq_top_or_exists`, `inf`, `isSubnormal_iff`, `lt_normal`, `map`, `normal_of_isSimpleAddGroup`, `of_subsingleton`, `quotient`, `trans`, `trans'`, `isSubnormal`, `bot`, `comap`, `eq_bot_or_top_of_isSimpleGroup`, `exists_chain`, `exists_normal_and_le_and_lt_top_of_ne`, `iff_eq_top_or_exists`, `inf`, `isSubnormal_iff`, `lt_normal`, `map`, `normal_of_isSimpleGroup`, `of_subsingleton`, `quotient`, `smul`, `subgroupOf`, `trans`, `trans'`, `isSubnormal`	34
Total	36

AddSubgroup

Definitions

Name	Category	Theorems
`IsSubnormal` 📖	CompData	12 math math: `IsSubnormal.quotient`, `IsSubnormal.inf`, `IsSubnormal.map`, `IsSubnormal.trans'`, `IsSubnormal.of_subsingleton`, `IsSubnormal.bot`, `Normal.isSubnormal`, `IsSubnormal.trans`, `IsSubnormal.addSubgroupOf`, `IsSubnormal.comap`, `IsSubnormal.iff_eq_top_or_exists`, `IsSubnormal.isSubnormal_iff`

AddSubgroup.IsSubnormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroupOf` 📖	mathematical	`AddSubgroup.IsSubnormal`	`AddSubgroup.IsSubnormal` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.addSubgroupOf`	—	`comap`
`bot` 📖	mathematical	—	`AddSubgroup.IsSubnormal` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`AddSubgroup.Normal.isSubnormal` `AddSubgroup.normal_bot`
`comap` 📖	mathematical	`AddSubgroup.IsSubnormal`	`AddSubgroup.IsSubnormal` `AddSubgroup.comap`	—	`AddSubgroup.comap_top` `AddSubgroup.comap_mono` `AddSubgroup.normal_addSubgroupOf_iff_le_normalizer` `LE.le.trans` `AddSubgroup.le_normalizer_comap`
`eq_bot_or_top_of_isSimpleAddGroup` 📖	mathematical	`AddSubgroup.IsSubnormal`	`Bot.bot` `AddSubgroup` `AddSubgroup.instBot` `Top.top` `AddSubgroup.instTop`	—	`AddSubgroup.Normal.eq_bot_or_eq_top` `normal_of_isSimpleAddGroup`
`exists_normal_and_le_and_lt_top_of_ne` 📖	mathematical	`AddSubgroup.IsSubnormal`	`AddSubgroup` `AddSubgroup.Normal` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Preorder.toLT` `Top.top` `AddSubgroup.instTop`	—	`eq_or_ne` `AddSubgroup.normalizer_eq_top_iff` `top_le_iff` `AddSubgroup.normal_addSubgroupOf_iff_le_normalizer` `le_rfl` `Ne.lt_top`
`iff_eq_top_or_exists` 📖	mathematical	—	`AddSubgroup.IsSubnormal` `Top.top` `AddSubgroup` `AddSubgroup.instTop` `Preorder.toLT` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.Normal` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.addSubgroupOf`	—	`not_top_lt` `AddSubgroup.normal_top` `eq_or_ne` `Ne.lt_top` `LE.le.lt_of_ne` `LT.lt.le`
`inf` 📖	mathematical	`AddSubgroup.IsSubnormal`	`AddSubgroup.IsSubnormal` `AddSubgroup` `AddSubgroup.instMin`	—	`AddSubgroup.addSubgroupOf_map_subtype` `trans'` `addSubgroupOf`
`isSubnormal_iff` 📖	mathematical	—	`AddSubgroup.IsSubnormal` `Monotone` `AddSubgroup` `Nat.instPreorder` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.Normal` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.addSubgroupOf` `Top.top` `AddSubgroup.instTop`	—	`monotone_nat_of_le_succ` `le_top` `AddSubgroup.addSubgroupOf_self` `AddSubgroup.normal_top`
`lt_normal` 📖	mathematical	`AddSubgroup.IsSubnormal`	`Top.top` `AddSubgroup` `AddSubgroup.instTop` `AddSubgroup.Normal` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Preorder.toLT`	—	`eq_or_ne` `top_le_iff` `AddSubgroup.normal_top` `lt_self_iff_false`
`map` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddSubgroup.IsSubnormal`	`AddSubgroup.IsSubnormal` `AddSubgroup.map`	—	`AddSubgroup.map_top_of_surjective` `AddSubgroup.map_mono` `AddSubgroup.normal_addSubgroupOf_of_le_normalizer` `LE.le.trans` `AddSubgroup.normal_addSubgroupOf_iff_le_normalizer` `AddSubgroup.le_normalizer_map`
`normal_of_isSimpleAddGroup` 📖	mathematical	`AddSubgroup.IsSubnormal`	`AddSubgroup.Normal`	—	`AddSubgroup.normal_top` `AddSubgroup.Normal.eq_bot_or_eq_top`
`of_subsingleton` 📖	mathematical	—	`AddSubgroup.IsSubnormal`	—	`AddSubgroup.eq_bot_of_subsingleton` `bot`
`quotient` 📖	mathematical	`AddSubgroup.IsSubnormal`	`AddSubgroup.IsSubnormal` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.map` `QuotientAddGroup.mk'`	—	`map` `QuotientAddGroup.mk'_surjective`
`trans` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.IsSubnormal` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.addSubgroupOf`	`AddSubgroup.IsSubnormal`	—	`trans'` `AddSubgroup.map_addSubgroupOf_eq_of_le`
`trans'` 📖	mathematical	`AddSubgroup.IsSubnormal` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup`	`AddSubgroup.IsSubnormal` `AddSubgroup.map` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.subtype`	—	`AddMonoidHom.range_eq_map` `AddSubgroup.range_subtype` `AddSubgroup.map_mono` `AddSubgroup.normal_addSubgroupOf_iff_le_normalizer` `le_trans` `AddSubgroup.le_normalizer_map`

AddSubgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSubnormal` 📖	mathematical	—	`AddSubgroup.IsSubnormal`	—	`le_top` `AddSubgroup.normal_addSubgroupOf`

Subgroup

Definitions

Name	Category	Theorems
`IsSubnormal` 📖	CompData	13 math math: `IsSubnormal.iff_eq_top_or_exists`, `IsSubnormal.comap`, `IsSubnormal.inf`, `IsSubnormal.smul`, `IsSubnormal.trans'`, `IsSubnormal.quotient`, `IsSubnormal.of_subsingleton`, `IsSubnormal.trans`, `IsSubnormal.map`, `IsSubnormal.bot`, `IsSubnormal.isSubnormal_iff`, `IsSubnormal.subgroupOf`, `Normal.isSubnormal`

Subgroup.IsSubnormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`Subgroup.IsSubnormal` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`Subgroup.Normal.isSubnormal` `Subgroup.normal_bot`
`comap` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup.IsSubnormal` `Subgroup.comap`	—	`Subgroup.comap_top` `Subgroup.comap_mono` `Subgroup.normal_subgroupOf_iff_le_normalizer` `LE.le.trans` `Subgroup.le_normalizer_comap`
`eq_bot_or_top_of_isSimpleGroup` 📖	mathematical	`Subgroup.IsSubnormal`	`Bot.bot` `Subgroup` `Subgroup.instBot` `Top.top` `Subgroup.instTop`	—	`Subgroup.Normal.eq_bot_or_eq_top` `normal_of_isSimpleGroup`
`exists_chain` 📖	mathematical	`Subgroup.IsSubnormal`	`Monotone` `Subgroup` `Nat.instPreorder` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.Normal` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subgroupOf` `Top.top` `Subgroup.instTop`	—	`isSubnormal_iff`
`exists_normal_and_le_and_lt_top_of_ne` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup` `Subgroup.Normal` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Preorder.toLT` `Top.top` `Subgroup.instTop`	—	`eq_or_ne` `Subgroup.normalizer_eq_top_iff` `top_le_iff` `Subgroup.normal_subgroupOf_iff_le_normalizer` `le_rfl` `Ne.lt_top`
`iff_eq_top_or_exists` 📖	mathematical	—	`Subgroup.IsSubnormal` `Top.top` `Subgroup` `Subgroup.instTop` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.Normal` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subgroupOf`	—	`eq_or_ne` `Ne.lt_top` `LE.le.lt_of_ne` `LT.lt.le`
`inf` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup.IsSubnormal` `Subgroup` `Subgroup.instMin`	—	`Subgroup.subgroupOf_map_subtype` `trans'` `subgroupOf`
`isSubnormal_iff` 📖	mathematical	—	`Subgroup.IsSubnormal` `Monotone` `Subgroup` `Nat.instPreorder` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.Normal` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subgroupOf` `Top.top` `Subgroup.instTop`	—	`monotone_nat_of_le_succ` `le_top` `Subgroup.subgroupOf_self`
`lt_normal` 📖	mathematical	`Subgroup.IsSubnormal`	`Top.top` `Subgroup` `Subgroup.instTop` `Subgroup.Normal` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Preorder.toLT`	—	`eq_or_ne`
`map` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Subgroup.IsSubnormal`	`Subgroup.IsSubnormal` `Subgroup.map`	—	`Subgroup.map_top_of_surjective` `Subgroup.map_mono` `Subgroup.normal_subgroupOf_of_le_normalizer` `LE.le.trans` `Subgroup.normal_subgroupOf_iff_le_normalizer` `Subgroup.le_normalizer_map`
`normal_of_isSimpleGroup` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup.Normal`	—	`Subgroup.Normal.eq_bot_or_eq_top`
`of_subsingleton` 📖	mathematical	—	`Subgroup.IsSubnormal`	—	`Subgroup.eq_bot_of_subsingleton`
`quotient` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup.IsSubnormal` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `QuotientGroup.Quotient.group` `Subgroup.map` `QuotientGroup.mk'`	—	`map` `QuotientGroup.mk'_surjective`
`smul` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup.IsSubnormal` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup.pointwiseMulAction`	—	`map` `MulAction.surjective`
`subgroupOf` 📖	mathematical	`Subgroup.IsSubnormal`	`Subgroup.IsSubnormal` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subgroupOf`	—	`comap`
`trans` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.IsSubnormal` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subgroupOf`	`Subgroup.IsSubnormal`	—	`trans'` `Subgroup.map_subgroupOf_eq_of_le`
`trans'` 📖	mathematical	`Subgroup.IsSubnormal` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Subgroup.IsSubnormal` `Subgroup.map` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.subtype`	—	`MonoidHom.range_eq_map` `Subgroup.range_subtype` `Subgroup.map_mono` `Subgroup.normal_subgroupOf_iff_le_normalizer` `le_trans` `Subgroup.le_normalizer_map`

Subgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSubnormal` 📖	mathematical	—	`Subgroup.IsSubnormal`	—	`le_top` `Subgroup.normal_subgroupOf`

---

← Back to Index