Basis

📁 Source: Mathlib/RingTheory/Ideal/Basis.lean

Statistics

Metric	Count
Definitions basisSpanSingleton	1
Theorems mem_ideal_iff, mem_ideal_iff', basisSpanSingleton_apply, constr_basisSpanSingleton	4
Total	5

Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_ideal_iff 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass CommSemiring.toSemiring Algebra.toSMul DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module' Algebra.toModule IsScalarTower.right Module.Basis.instFunLike	—	IsScalarTower.right Module.Basis.mem_submodule_iff RingHomInvPair.ids LinearMap.IsScalarTower.compatibleSMul Submodule.restrictScalars.isScalarTower Submodule.isScalarTower' IsScalarTower.left
mem_ideal_iff' 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Finset.sum Finset.univ Algebra.toSMul DFunLike.coe Module.Basis CommSemiring.toSemiring Submodule.addCommMonoid Submodule.module' Algebra.toModule IsScalarTower.right Module.Basis.instFunLike	—	IsScalarTower.right Module.Basis.mem_submodule_iff' RingHomInvPair.ids LinearMap.IsScalarTower.compatibleSMul Submodule.restrictScalars.isScalarTower Submodule.isScalarTower' IsScalarTower.left

Ideal

Definitions

Name	Category	Theorems
basisSpanSingleton 📖	CompOp	2 math math: basisSpanSingleton_apply, constr_basisSpanSingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisSpanSingleton_apply 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule span Set Set.instSingletonSet DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right Module.Basis.instFunLike basisSpanSingleton Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
constr_basisSpanSingleton 📖	mathematical	—	AddHom.toFun LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommRing.toCommSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Pi.addCommMonoid LinearMap.addCommMonoid LinearMap.toAddHom Pi.Function.module LinearMap.module LinearEquiv.toLinearMap RingHomInvPair.ids Module.Basis.constr Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule span Set Set.instSingletonSet DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module' Algebra.toSMul IsScalarTower.right Module.Basis.instFunLike basisSpanSingleton AlgHom Module.End Module.End.instSemiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike Algebra.lmul	—	Module.Basis.ext RingHomInvPair.ids IsScalarTower.right smulCommClass_self IsScalarTower.left Module.Basis.constr_basis basisSpanSingleton_apply

---

← Back to Index