Structures · Algebra
AddSubgroupClass
AddSubgroupClass S G states S is a type of subsets s ⊆ G that are
additive subgroups of G.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances10
- LieSubalgebra
- LieSubmodule
- AddSubgroup
- TwoSidedIdeal
- OpenAddSubgroup
- OpenNormalAddSubgroup
- FiniteIndexNormalAddSubgroup
- ClosedAddSubgroup
- LieRinehartSubalgebra
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by351
- AlgebraicGeometry.Proj
- sub_mem
- AlgebraicGeometry.Proj.basicOpen
- AlgebraicGeometry.Proj.awayι
- HomogeneousLocalization.awayMap
- AlgebraicGeometry.Proj.toLocallyRingedSpace
- AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf
- AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction
- zsmul_mem
- AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec
- AlgebraicGeometry.Proj.pullbackAwayιIso
- AlgebraicGeometry.Proj.basicOpenIsoSpec
- HomogeneousLocalization.Away.map
- add_mem_cancel_right
- AlgebraicGeometry.Proj.map
- AlgebraicGeometry.Proj.awayToSection
- AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier
- AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec
- HomogeneousLocalization.val_mul
- add_mem_cancel_left
- AlgebraicGeometry.ProjectiveSpectrum.comap
- AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections
- HomogeneousLocalization.fromZeroRingHom
- HomogeneousLocalization.mapId
- AlgebraicGeometry.Proj.stalkIso'
- HomogeneousLocalization.val_zero
- AlgebraicGeometry.Proj.fromOfGlobalSections
- AlgebraicGeometry.sectionInBasicOpen
- HomogeneousLocalization.val_one
- AddSubgroupClass.coe_sub
- AlgebraicGeometry.mem_basicOpen_den
- HomogeneousLocalization.NumDenSameDeg.map
- AlgebraicGeometry.Proj.basicOpen_mono
- AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier
- AlgebraicGeometry.Proj.toSpecZero
- AlgebraicGeometry.Proj.SpecMap_awayMap_awayι
- AlgebraicGeometry.Proj.basicOpenToSpec
- AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isFractionPrelocal
- HomogeneousLocalization.map
- AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ
- HomogeneousLocalization.Away.isLocalizationElem
- HomogeneousLocalization.localRingHom
- AlgebraicGeometry.Proj.toSheafedSpace
- AddSubgroupClass.inclusion
- AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier
- AlgebraicGeometry.Proj.sheafedSpaceMap
- AlgebraicGeometry.Proj.affineOpenCover
- HomogeneousLocalization.val_pow
- AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun
- AlgebraicGeometry.stalkToFiberRingHom