Theorems · Theorem · group theory
PSL.iSup_iwasawaT_eq_top
∀ {F : Type u_2} [inst : Field F], iSup PSL.iwasawaT = ⊤The Iwasawa generator property: when Fintype.card ι = 2, the supremum of the
iwasawaT subgroups equals all of PSL.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
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.
- Top.topstatement and proof · cited by 9,680
- Fieldstatement and proof · cited by 7,404
- Subgroupstatement and proof · cited by 3,593
- iSupstatement and proof · cited by 2,415
- HasQuotient.Quotientproof · cited by 2,301
- Matrix.SpecialLinearGroupstatement and proof · cited by 348
- Subgroup.mapproof · cited by 301
- Subgroup.centerstatement and proof · cited by 121
- Projectivizationstatement and proof · cited by 111
- QuotientGroup.mk'proof · cited by 90
- QuotientGroup.mk'_surjectiveproof · cited by 15
- Projectivization.submoduleproof · cited by 11
Cited by1
Results whose statement or proof uses this declaration.
- PSL2.Iwasawaproof · cited by 1