Iwasawa

📁 Source: Mathlib/GroupTheory/GroupAction/Iwasawa.lean

Statistics

Metric	Count
Definitions IwasawaStructure, T	2
Theorems commutator_le, isSimpleGroup, is_comm, is_conj, is_generator	5
Total	7

MulAction

Definitions

Name	Category	Theorems
IwasawaStructure 📖	CompData	—

MulAction.IwasawaStructure

Definitions

Name	Category	Theorems
T 📖	CompOp	3 math math: is_generator, is_comm, is_conj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutator_le 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder commutator	—	MulAction.IsQuasiPreprimitive.isPretransitive_of_normal MulAction.nontrivial_of_fixedPoints_ne_univ Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top Nontrivial.to_nonempty eq_top_iff is_generator iSup_le_iff MulAction.exists_smul_eq Subgroup.smul_def is_conj Subgroup.mem_sup_left Subtype.mem Subgroup.mem_sup_right Subgroup.mul_mem Subgroup.inv_mem is_comm
isSimpleGroup 📖	mathematical	commutator Top.top Subgroup Subgroup.instTop	IsSimpleGroup	—	commutator_le Subgroup.eq_bot_iff_forall FaithfulSMul.eq_of_smul_eq_smul one_smul Set.eq_univ_iff_forall top_le_iff le_trans ge_of_eq
is_comm 📖	mathematical	—	IsMulCommutative Subgroup SetLike.instMembership Subgroup.instSetLike T Subgroup.mul	—	—
is_conj 📖	mathematical	—	T SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Subgroup MulAut.instGroup Subgroup.pointwiseMulAction MulAut.applyMulDistribMulAction DFunLike.coe MonoidHom MonoidHom.instFunLike MulAut.conj	—	—
is_generator 📖	mathematical	—	iSup Subgroup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice T Top.top Subgroup.instTop	—	—

---

← Back to Index