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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass IsScalarTower.right Algebra.TensorProduct.map AlgHom.id	—	IsScalarTower.to_smulCommClass IsScalarTower.right Algebra.TensorProduct.map_surjective IsScalarTower.left

---

← Back to Index