Basic

📁 Source: Mathlib/RingTheory/GradedAlgebra/Basic.lean

Statistics

Metric	Count
Definitions `coeAlgEquiv`, `gradedAlgebra`, `decomposeAlgEquiv`, `decomposeRingEquiv`, `GradedAlgebra`, `ofAlgHom`, `proj`, `GradedRing`, `proj`, `projZeroRingHom`, `projZeroRingHom'`, `toDecomposition`, `instGradedAlgebraRestrictScalars`	13
Theorems `coe_decompose_mul_add_of_left_mem`, `coe_decompose_mul_add_of_right_mem`, `coe_decompose_mul_of_left_mem`, `coe_decompose_mul_of_left_mem_of_le`, `coe_decompose_mul_of_left_mem_of_not_le`, `coe_decompose_mul_of_left_mem_zero`, `coe_decompose_mul_of_right_mem`, `coe_decompose_mul_of_right_mem_of_le`, `coe_decompose_mul_of_right_mem_of_not_le`, `coe_decompose_mul_of_right_mem_zero`, `decomposeAlgEquiv_apply`, `decomposeAlgEquiv_symm_apply`, `decompose_algebraMap`, `decompose_mul`, `decompose_mul_add_left`, `decompose_mul_add_right`, `decompose_one`, `decompose_symm_algebraMap`, `decompose_symm_mul`, `decompose_symm_one`, `mem_support_iff`, `proj_apply`, `proj_recompose`, `coe_projZeroRingHom'_apply`, `mem_support_iff`, `projZeroRingHom'_apply_coe`, `projZeroRingHom'_surjective`, `projZeroRingHom_apply`, `proj_apply`, `proj_recompose`, `toGradedMonoid`	31
Total	44

DirectSum

Definitions

Name	Category	Theorems
`decomposeAlgEquiv` 📖	CompOp	2 math math: `decomposeAlgEquiv_symm_apply`, `decomposeAlgEquiv_apply`
`decomposeRingEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_decompose_mul_add_of_left_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddLeftCancelMonoid.toAddMonoid` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_of_mul_apply_add`
`coe_decompose_mul_add_of_right_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddRightCancelMonoid.toAddMonoid` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_mul_of_apply_add`
`coe_decompose_mul_of_left_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_of_mul_apply`
`coe_decompose_mul_of_left_mem_of_le` 📖	mathematical	`SetLike.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_of_mul_apply_of_le`
`coe_decompose_mul_of_left_mem_of_not_le` 📖	mathematical	`SetLike.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_of_mul_apply_of_not_le`
`coe_decompose_mul_of_left_mem_zero` 📖	mathematical	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_of_mul_apply_of_mem_zero`
`coe_decompose_mul_of_right_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_mul_of_apply`
`coe_decompose_mul_of_right_mem_of_le` 📖	mathematical	`SetLike.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_mul_of_apply_of_le`
`coe_decompose_mul_of_right_mem_of_not_le` 📖	mathematical	`SetLike.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_mul_of_apply_of_not_le`
`coe_decompose_mul_of_right_mem_zero` 📖	mathematical	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CanLift.prf` `Subtype.canLift` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `decompose_mul` `decompose_coe` `coe_mul_of_apply_of_mem_zero`
`decomposeAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `DirectSum` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `semiring` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `GradedRing.toGradedMonoid` `instAlgebra` `Submodule.module` `Submodule.galgebra` `AlgEquiv.instFunLike` `decomposeAlgEquiv` `Equiv` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition`	—	`Submodule.addSubmonoidClass` `GradedRing.toGradedMonoid`
`decomposeAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `DirectSum` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `semiring` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `GradedRing.toGradedMonoid` `instAlgebra` `Submodule.module` `Submodule.galgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `decomposeAlgEquiv` `Equiv` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `GradedRing.toDecomposition`	—	`Submodule.addSubmonoidClass` `GradedRing.toGradedMonoid`
`decompose_algebraMap` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `RingHom` `RingHom.instFunLike` `algebraMap` `Submodule.addCommMonoid` `semiring` `SetLike.gsemiring` `GradedRing.toGradedMonoid` `instAlgebra` `Submodule.module` `Submodule.galgebra`	—	`AlgEquiv.commutes` `Submodule.addSubmonoidClass` `GradedRing.toGradedMonoid`
`decompose_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `GradedRing.toGradedMonoid`	—	`map_mul` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass`
`decompose_mul_add_left` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `AddLeftCancelMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMul.mul` `SetLike.gMul` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `GradedRing.toGradedMonoid`	—	`SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `coe_decompose_mul_add_of_left_mem`
`decompose_mul_add_right` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `AddRightCancelMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMul.mul` `SetLike.gMul` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `GradedRing.toGradedMonoid`	—	`SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `coe_decompose_mul_add_of_right_mem`
`decompose_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SetLike.gOne` `SetLike.GradedMonoid.toGradedOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `GradedRing.toGradedMonoid`	—	`map_one` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`decompose_symm_algebraMap` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `GradedRing.toDecomposition` `RingHom` `Submodule.addCommMonoid` `semiring` `SetLike.gsemiring` `GradedRing.toGradedMonoid` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Submodule.module` `Submodule.galgebra`	—	`AlgEquiv.commutes` `Submodule.addSubmonoidClass` `GradedRing.toGradedMonoid`
`decompose_symm_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `GradedRing.toDecomposition` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `GradedRing.toGradedMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`map_mul` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass`
`decompose_symm_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompose` `GradedRing.toDecomposition` `instOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SetLike.gOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SetLike.GradedMonoid.toGradedOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `GradedRing.toGradedMonoid`	—	`map_one` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`

DirectSum.IsInternal

Definitions

Name	Category	Theorems
`coeAlgEquiv` 📖	CompOp	—
`gradedAlgebra` 📖	CompOp	—

GradedAlgebra

Definitions

Name	Category	Theorems
`ofAlgHom` 📖	CompOp	—
`proj` 📖	CompOp	2 math math: `proj_recompose`, `proj_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_support_iff` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `DFinsupp.support` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.setLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition`	—	`Submodule.addSubmonoidClass` `DFinsupp.mem_support_iff` `Iff.not` `Submodule.coe_eq_zero`
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `proj` `Submodule` `SetLike.instMembership` `Submodule.setLike` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition`	—	—
`proj_recompose` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `proj` `Equiv` `DirectSum` `Submodule` `SetLike.instMembership` `Submodule.setLike` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `DirectSum.decompose` `GradedRing.toDecomposition` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.of` `DFinsupp` `AddZero.toZero` `DFinsupp.instDFunLike`	—	`Submodule.addSubmonoidClass` `proj_apply` `DirectSum.decompose_symm_of` `Equiv.apply_symm_apply`

GradedRing

Definitions

Name	Category	Theorems
`proj` 📖	CompOp	14 math math: `Ideal.isHomogeneous_iff_subset_iInter`, `Ideal.isHomogeneous_iff_forall_subset`, `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff'`, `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff`, `HomogeneousIdeal.mem_irrelevant_iff`, `Ideal.homogeneousHull_eq_iSup`, `Ideal.mul_homogeneous_element_mem_of_mem`, `Subsemiring.isHomogeneous_iff_subset_iInter`, `Subsemiring.isHomogeneous_iff_forall_subset`, `AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj`, `ProjectiveSpectrum.basicOpen_eq_union_of_projection`, `Ideal.toIdeal_homogeneousHull_eq_iSup`, `proj_apply`, `proj_recompose`
`projZeroRingHom` 📖	CompOp	3 math math: `projZeroRingHom_apply`, `HomogeneousIdeal.toIdeal_irrelevant`, `coe_projZeroRingHom'_apply`
`projZeroRingHom'` 📖	CompOp	3 math math: `projZeroRingHom'_apply_coe`, `projZeroRingHom'_surjective`, `coe_projZeroRingHom'_apply`
`toDecomposition` 📖	CompOp	51 math math: `DirectSum.decomposeAlgEquiv_symm_apply`, `HomogeneousIdeal.toAddSubmonoid_irrelevant_le`, `DirectSum.coe_decompose_mul_add_of_left_mem`, `DirectSum.coe_decompose_mul_of_left_mem_of_le`, `DirectSum.decompose_symm_one`, `DirectSum.coe_decompose_mul_of_left_mem`, `GradedAlgebra.proj_recompose`, `HomogeneousIdeal.irrelevant_le`, `AlgebraicGeometry.Proj.sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier`, `DirectSum.decompose_mul_add_left`, `IsHomogeneous.subsemiringClosure`, `Ideal.homogeneousHull_eq_iSup`, `DirectSum.decompose_symm_algebraMap`, `Subsemiring.isHomogeneous_iff_subset_iInter`, `DirectSum.coe_decompose_mul_of_right_mem_of_not_le`, `DirectSum.coe_decompose_mul_of_left_mem_of_not_le`, `DirectSum.decompose_algebraMap`, `AddMonoidAlgebra.GradesBy.decompose_single`, `mem_support_iff`, `DirectSum.coe_decompose_mul_of_right_mem`, `Subsemiring.isHomogeneous_iff_forall_subset`, `GradedTensorProduct.auxEquiv_tmul`, `coe_toIdeal`, `DirectSum.coe_decompose_mul_add_of_right_mem`, `toIdeal_le_toIdeal_iff`, `HomogeneousSubsemiring.isHomogeneous`, `DirectSum.decomposeAlgEquiv_apply`, `AddMonoidAlgebra.grade.decompose_single`, `map_directSumDecompose`, `DirectSum.SetLike.IsHomogeneous.mem_iff`, `DirectSum.decompose_symm_mul`, `HomogeneousSubsemiring.is_homogeneous'`, `GradedRingHom.map_directSumDecompose`, `GradedAlgebra.proj_apply`, `projZeroRingHom_apply`, `HomogeneousIdeal.irrelevant_eq_iSup`, `DirectSum.decompose_map`, `DirectSum.decompose_mul`, `DirectSum.decompose_one`, `DirectSum.decompose_mul_add_right`, `HomogeneousIdeal.irrelevant_eq_closure`, `AddMonoidAlgebra.decomposeAux_eq_decompose`, `DirectSum.coe_decompose_mul_of_left_mem_zero`, `DirectSum.coe_decompose_mul_of_right_mem_of_le`, `DirectSum.coe_decompose_mul_of_right_mem_zero`, `GradedAlgebra.mem_support_iff`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen`, `IsHomogeneous.subsemiringClosure_of_isHomogeneousElem`, `proj_apply`, `proj_recompose`, `Ideal.IsHomogeneous.mem_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_projZeroRingHom'_apply` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SetLike.GradeZero.instSemiring` `toGradedMonoid` `RingHom.instFunLike` `projZeroRingHom'` `projZeroRingHom`	—	`toGradedMonoid`
`mem_support_iff` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `DFinsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `toDecomposition`	—	`AddSubmonoidClass.toZeroMemClass` `DFinsupp.mem_support_iff` `Iff.not` `ZeroMemClass.coe_eq_zero`
`projZeroRingHom'_apply_coe` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Semiring.toNonAssocSemiring` `SetLike.GradeZero.instSemiring` `toGradedMonoid` `RingHom.instFunLike` `projZeroRingHom'`	—	`toGradedMonoid` `DirectSum.decompose_coe` `DirectSum.of_eq_same`
`projZeroRingHom'_surjective` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SetLike.GradeZero.instSemiring` `toGradedMonoid` `RingHom.instFunLike` `projZeroRingHom'`	—	`toGradedMonoid` `projZeroRingHom'_apply_coe`
`projZeroRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `projZeroRingHom` `SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `toDecomposition`	—	—
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `proj` `SetLike.instMembership` `DFinsupp` `AddZero.toZero` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `toDecomposition`	—	—
`proj_recompose` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `proj` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `DirectSum.decompose` `toDecomposition` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `DirectSum.of` `DFinsupp` `AddZero.toZero` `DFinsupp.instDFunLike`	—	`proj_apply` `DirectSum.decompose_symm_of` `Equiv.apply_symm_apply`
`toGradedMonoid` 📖	mathematical	—	`SetLike.GradedMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—

(root)

Definitions

Name	Category	Theorems
`GradedAlgebra` 📖	CompOp	—
`GradedRing` 📖	CompData	—
`instGradedAlgebraRestrictScalars` 📖	CompOp	8 math math: `GradedAlgHom.coe_restrictScalars`, `GradedAlgHom.restrictScalars_coe_algHom`, `GradedAlgHom.includeRight_apply`, `GradedAlgHom.restrictScalars_coe_linearMap`, `GradedAlgHom.restrictScalars_apply`, `GradedAlgHom.liftEquiv_symm_apply`, `GradedAlgHom.liftEquiv_tmul`, `GradedAlgHom.restrictScalars_injective`

---

← Back to Index