FiniteStability

📁 Source: Mathlib/RingTheory/FiniteStability.lean

Statistics

Metric	Count
Definitions	0
Theorems baseChange, baseChange, baseChangeAux_surj	3
Total	3

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	—	Algebra.FinitePresentation TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass RingHom.instRingHomClass IsScalarTower.right Algebra.FiniteType.baseChangeAux_surj AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.TensorProduct.lTensor_ker Ideal.FG.map Ideal.fg_ker_comp AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass RingHom.ker_equiv AlgEquivClass.toRingEquivClass Submodule.fg_bot EquivLike.surjective

Algebra.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	—	Algebra.FiniteType TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass iff_quotient_mvPolynomial'' IsScalarTower.right baseChangeAux_surj
baseChangeAux_surj 📖	mathematical	MvPolynomial CommRing.toCommSemiring DFunLike.coe AlgHom AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike	TensorProduct CommRing.toCommSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Algebra.toModule AddMonoidAlgebra.algebra Algebra.id DFunLike.coe AlgHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass IsScalarTower.right AlgHom.funLike Algebra.TensorProduct.map AlgHom.id	—	IsScalarTower.to_smulCommClass IsScalarTower.right Algebra.TensorProduct.map_surjective IsScalarTower.left

---

← Back to Index