NoetherNormalization

📁 Source: Mathlib/RingTheory/NoetherNormalization.lean

Statistics

Metric	Count
Definitions T1	1
Theorems exists_finite_inj_algHom_of_fg, exists_integral_inj_algHom_of_fg, exists_integral_inj_algHom_of_quotient	3
Total	4

NoetherNormalization

Definitions

Name	Category	Theorems
T1 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_inj_algHom_of_fg 📖	mathematical	—	MvPolynomial Semifield.toCommSemiring Field.toSemifield DFunLike.coe AlgHom CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike AlgHom.Finite EuclideanDomain.toCommRing Field.toEuclideanDomain MvPolynomial.instCommRingMvPolynomial	—	exists_integral_inj_algHom_of_fg IsScalarTower.algebraMap_eq IsScalarTower.of_algHom RingHom.algebraMap_toAlgebra' RingHom.IsIntegral.to_finite RingHom.FiniteType.of_comp_finiteType RingHom.finiteType_algebraMap
exists_integral_inj_algHom_of_fg 📖	mathematical	—	MvPolynomial Semifield.toCommSemiring Field.toSemifield DFunLike.coe AlgHom CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike RingHom.IsIntegral MvPolynomial.instCommRingMvPolynomial EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing AlgHom.toRingHom	—	Algebra.FiniteType.iff_quotient_mvPolynomial'' AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instIsTwoSidedKer exists_integral_inj_algHom_of_quotient RingHom.ker_ne_top AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass EquivLike.toEmbeddingLike RingHom.IsIntegral.trans RingHom.isIntegral_of_surjective AlgEquiv.surjective
exists_integral_inj_algHom_of_quotient 📖	mathematical	—	MvPolynomial Semifield.toCommSemiring Field.toSemifield HasQuotient.Quotient Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe AlgHom Ideal.Quotient.semiring MvPolynomial.algebra Algebra.id Ideal.instAlgebraQuotient AlgHom.funLike RingHom.IsIntegral Ideal.Quotient.instRingQuotient AlgHom.toRingHom	—	le_rfl Ideal.instIsTwoSided_1 MvPolynomial.eq_C_of_isEmpty Fin.isEmpty' sub_ne_zero_of_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isUnit_iff_exists Ne.isUnit MvPolynomial.smul_eq_C_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MvPolynomial.C_1 Ideal.eq_top_iff_one Submodule.smul_of_tower_mem IsScalarTower.right Ideal.Quotient.eq RingHom.isIntegral_of_surjective Ideal.Quotient.mkₐ_surjective Ideal.Quotient.mk_bijective_iff_eq_bot Submodule.exists_mem_ne_zero_of_ne_bot AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instIsTwoSidedKer Ideal.Quotient.nontrivial_iff RingHom.ker_ne_top AlgHom.ext Ideal.kerLiftAlg_injective AlgHom.coe_comp RingHom.IsIntegral.trans RingHom.IsIntegral.tower_top

---

← Back to Index