IsSubnormal

📁 Source: Mathlib/GroupTheory/IsSubnormal.lean

Statistics

Metric	Count
Definitions IsSubnormal, IsSubnormal	2
Theorems bot, eq_bot_or_top_of_isSimpleAddGroup, exists_normal_and_le_and_lt_top_of_ne, iff_eq_top_or_exists, isSubnormal_iff, lt_normal, normal_of_isSimpleAddGroup, trans, trans', isSubnormal, bot, eq_bot_or_top_of_isSimpleGroup, exists_chain, exists_normal_and_le_and_lt_top_of_ne, iff_eq_top_or_exists, isSubnormal_iff, lt_normal, normal_of_isSimpleGroup, trans, trans', isSubnormal	21
Total	23

AddSubgroup

Definitions

Name	Category	Theorems
IsSubnormal 📖	CompData	4 math math: IsSubnormal.bot, Normal.isSubnormal, IsSubnormal.iff_eq_top_or_exists, IsSubnormal.isSubnormal_iff

AddSubgroup.IsSubnormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot 📖	mathematical	—	AddSubgroup.IsSubnormal Bot.bot AddSubgroup AddSubgroup.instBot	—	AddSubgroup.Normal.isSubnormal AddSubgroup.normal_bot
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.Normal AddSubgroup 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
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
normal_of_isSimpleAddGroup 📖	mathematical	AddSubgroup.IsSubnormal	AddSubgroup.Normal	—	AddSubgroup.normal_top AddSubgroup.Normal.eq_bot_or_eq_top
trans 📖	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.IsSubnormal SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup AddSubgroup.addSubgroupOf	—	—	trans' AddSubgroup.map_addSubgroupOf_eq_of_le
trans' 📖	mathematical	AddSubgroup.IsSubnormal AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup	AddSubgroup.map 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	4 math math: IsSubnormal.iff_eq_top_or_exists, IsSubnormal.bot, IsSubnormal.isSubnormal_iff, 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
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.Normal Subgroup 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
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
normal_of_isSimpleGroup 📖	mathematical	Subgroup.IsSubnormal	Subgroup.Normal	—	Subgroup.Normal.eq_bot_or_eq_top
trans 📖	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.IsSubnormal SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subgroupOf	—	—	trans' Subgroup.map_subgroupOf_eq_of_le
trans' 📖	mathematical	Subgroup.IsSubnormal Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	Subgroup.map 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