Basic

📁 Source: Mathlib/RingTheory/Extension/Presentation/Basic.lean

Statistics

Metric	Count
Definitions baseChange, comp, compRelationAux, dimension, id, localizationAway, naive, ofAlgEquiv, ofBijectiveAlgebraMap, ofFinitePresentation, ofFinitePresentationRels, ofFinitePresentationVars, quotientEquiv, reindex, relation, toGenerators	16
Theorems C_mul_X_sub_one_mem_ker, fg_ker_of_finitePresentation, ker_localizationAway, aeval_val_relation, baseChange_relation, baseChange_toGenerators, comp_aeval_relation_inl, comp_relation, comp_relation_inr, dimension_ofAlgEquiv, dimension_reindex, exists_presentation_fin, fg_ker, finitePresentation_of_isFinite, id_dimension, instFinitePresentationQuotientOfFinite, localizationAway_dimension_zero, localizationAway_relation, mem_ker_naive, naive_relation, naive_relation_apply, naive_toGenerators, ofAlgEquiv_relation, ofAlgEquiv_toGenerators, ofBijectiveAlgebraMap_dimension, quotientEquiv_mk, quotientEquiv_symm, reindex_toGenerators, relation_comp_localizationAway_inl, relation_mem_ker, span_range_relation_eq_ker, toGenerators_comp	32
Total	48

Algebra.Generators

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_mul_X_sub_one_mem_ker 📖	mathematical	—	Ring localizationAway Ideal CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker MvPolynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom RingHom.instFunLike MvPolynomial.C MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Algebra.Presentation.relation_mem_ker
fg_ker_of_finitePresentation 📖	mathematical	—	Ideal.FG Ring CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring ker	—	AlgHomClass.toRingHomClass AlgHom.algHomClass ker_eq_ker_aeval_val Algebra.FinitePresentation.ker_fG_of_surjective aeval_val_surjective Algebra.FinitePresentation.mvPolynomial Algebra.FinitePresentation.self
ker_localizationAway 📖	mathematical	—	ker localizationAway Ideal.span Ring CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring Set Set.instSingletonSet MvPolynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.C MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Ideal.instIsTwoSided_1 MvPolynomial.algHom_ext MvPolynomial.aeval_X IsLocalization.Away.mvPolynomialQuotientEquiv_apply AlgHomClass.toRingHomClass AlgHom.algHomClass ker_eq_ker_aeval_val AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.toAlgHom_eq_coe RingHom.instRingHomClass RingHom.ker_coe_toRingHom AlgHom.comp_toRingHom RingHom.comap_ker Ideal.comap.congr_simp RingHom.ker_equiv AlgEquivClass.toRingEquivClass Ideal.Quotient.mkₐ_ker

Algebra.Presentation

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	3 math math: Algebra.PreSubmersivePresentation.baseChange_toPresentation, baseChange_relation, baseChange_toGenerators
comp 📖	CompOp	6 math math: comp_relation_inr, comp_aeval_relation_inl, comp_relation, toGenerators_comp, relation_comp_localizationAway_inl, Algebra.PreSubmersivePresentation.toPresentation_comp
compRelationAux 📖	CompOp	1 math math: comp_relation
dimension 📖	CompOp	8 math math: dimension_ofAlgEquiv, Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension, ofBijectiveAlgebraMap_dimension, Algebra.SubmersivePresentation.rank_kaehlerDifferential, localizationAway_dimension_zero, id_dimension, Algebra.IsStandardSmoothOfRelativeDimension.out, dimension_reindex
id 📖	CompOp	1 math math: id_dimension
localizationAway 📖	CompOp	3 math math: localizationAway_relation, relation_comp_localizationAway_inl, localizationAway_dimension_zero
naive 📖	CompOp	5 math math: naive_toGenerators, naive_relation, naive_relation_apply, Algebra.PreSubmersivePresentation.naive_toPresentation, mem_ker_naive
ofAlgEquiv 📖	CompOp	4 math math: dimension_ofAlgEquiv, ofAlgEquiv_relation, Algebra.PreSubmersivePresentation.ofAlgEquiv_toPresentation, ofAlgEquiv_toGenerators
ofBijectiveAlgebraMap 📖	CompOp	1 math math: ofBijectiveAlgebraMap_dimension
ofFinitePresentation 📖	CompOp	—
ofFinitePresentationRels 📖	CompOp	—
ofFinitePresentationVars 📖	CompOp	—
quotientEquiv 📖	CompOp	2 math math: quotientEquiv_symm, quotientEquiv_mk
reindex 📖	CompOp	3 math math: reindex_toGenerators, Algebra.PreSubmersivePresentation.reindex_toPresentation, dimension_reindex
relation 📖	CompOp	32 math math: localizationAway_relation, differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, comp_relation_inr, map_relationOfHasCoeffs, Algebra.Generators.exists_presentation_of_free_cotangent, naive_relation, Algebra.SubmersivePresentation.ofSubsingleton_relation, coeffs_relation_subset_coeffs, comp_aeval_relation_inl, Algebra.SubmersivePresentation.jacobianRelations_spec, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, coeffs_relation_subset_core, naive_relation_apply, span_range_relation_eq_ker, comp_relation, aeval_val_relation, relation_mem_ker, MvPolynomial.universalFactorizationMapPresentation_relation, Algebra.PreSubmersivePresentation.aevalDifferential_single, ofAlgEquiv_relation, relation_comp_localizationAway_inl, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, algebraTensorAlgEquiv_symm_relation, HasCoeffs.relation_mem_range_map, baseChange_relation, StandardEtalePresentation.toPresentation_relation, Algebra.SubmersivePresentation.basisCotangent_apply, HasCoeffs.coeffs_relation_mem_range, Algebra.SubmersivePresentation.basisDeriv_apply
toGenerators 📖	CompOp	76 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, differentials.comm₁₂_single, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, naive_toGenerators, differentials.comm₂₃, StandardEtalePresentation.toPresentation_algebra_smul, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', quotientEquiv_symm, Algebra.Generators.exists_presentation_of_free_cotangent, comp_aeval_relation_inl, Algebra.SubmersivePresentation.jacobianRelations_spec, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, differentials.surjective_hom₁, span_range_relation_eq_ker, comp_relation, toGenerators_comp, aeval_val_relation, differentials.comm₂₃', fg_ker, relation_mem_ker, Algebra.SubmersivePresentation.subsingleton_h1Cotangent, Algebra.PreSubmersivePresentation.aevalDifferential_single, Algebra.SubmersivePresentation.ofSubsingleton_val, tensorModelOfHasCoeffsEquiv_tmul, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, tensorModelOfHasCoeffsHom_tmul, differentials.comm₁₂, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, aeval_val_relationOfHasCoeffs, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, reindex_toGenerators, StandardEtalePresentation.toPresentation_σ', Algebra.SubmersivePresentation.cotangentComplexAux_surjective, Algebra.SubmersivePresentation.basisKaehler_apply, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, StandardEtalePresentation.aeval_val_equivMvPolynomial, tensorModelOfHasCoeffsEquiv_symm_tmul, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, StandardEtalePresentation.toPresentation_val, Algebra.SubmersivePresentation.ofSubsingleton_σ', ofAlgEquiv_toGenerators, HasCoeffs.relation_mem_range_map, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, Algebra.SubmersivePresentation.sectionCotangent_comp, MvPolynomial.universalFactorizationMapPresentation_val, MvPolynomial.universalFactorizationMapPresentation_σ', quotientEquiv_mk, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, Algebra.SubmersivePresentation.free_cotangent, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.SubmersivePresentation.basisCotangent_apply, instFinitePresentationQuotientOfFinite, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, Algebra.SubmersivePresentation.cotangentEquiv_apply, Algebra.PreSubmersivePresentation.baseChange_ring, Algebra.SubmersivePresentation.basisDeriv_apply, mem_ker_naive, baseChange_toGenerators, Algebra.PreSubmersivePresentation.toGenerators_comp, tensorModelOfHasCoeffsInv_aeval_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_val_relation 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val toGenerators relation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.mem_ker Algebra.Generators.ker_eq_ker_aeval_val span_range_relation_eq_ker Ideal.subset_span
baseChange_relation 📖	mathematical	—	relation TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass baseChange DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map algebraMap	—	Algebra.to_smulCommClass
baseChange_toGenerators 📖	mathematical	—	toGenerators TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass baseChange Algebra.Generators.baseChange	—	Algebra.to_smulCommClass
comp_aeval_relation_inl 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval MvPolynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.C Algebra.Generators.val toGenerators relation comp	—	—
comp_relation 📖	mathematical	—	relation comp Algebra.Generators.Ring Algebra.Generators.comp toGenerators compRelationAux DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename	—	—
comp_relation_inr 📖	mathematical	—	relation comp DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename	—	—
dimension_ofAlgEquiv 📖	mathematical	—	dimension ofAlgEquiv	—	—
dimension_reindex 📖	mathematical	—	dimension reindex	—	Nat.card_congr
exists_presentation_fin 📖	mathematical	—	Algebra.Presentation	—	RingHom.instRingHomClass Algebra.FinitePresentation.out AlgHomClass.toRingHomClass AlgHom.algHomClass Submodule.fg_iff_exists_fin_generating_family MvPolynomial.algHom_ext MvPolynomial.aeval_X
fg_ker 📖	mathematical	—	Ideal.FG Algebra.Generators.Ring toGenerators CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring Algebra.Generators.ker	—	Set.finite_range Set.Finite.coe_toFinset span_range_relation_eq_ker
finitePresentation_of_isFinite 📖	mathematical	—	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	Algebra.FinitePresentation.equiv instFinitePresentationQuotientOfFinite Ideal.Quotient.isScalarTower IsScalarTower.right Algebra.Generators.instIsScalarTowerRing IsScalarTower.left
id_dimension 📖	mathematical	—	dimension Algebra.id CommRing.toCommSemiring id	—	ofBijectiveAlgebraMap_dimension Function.bijective_id
instFinitePresentationQuotientOfFinite 📖	mathematical	—	Algebra.FinitePresentation Quotient CommRing.toCommSemiring Ideal.Quotient.semiring Algebra.Generators.Ring toGenerators MvPolynomial.instCommRingMvPolynomial Algebra.Generators.ker Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id	—	Algebra.FinitePresentation.quotient fg_ker Algebra.FinitePresentation.mvPolynomial Algebra.FinitePresentation.self
localizationAway_dimension_zero 📖	mathematical	—	dimension localizationAway	—	Nat.card_eq_fintype_card Fintype.card_unique tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub
localizationAway_relation 📖	mathematical	—	relation localizationAway MvPolynomial CommRing.toCommSemiring Algebra.Generators.Ring Algebra.Generators.localizationAway SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	—
mem_ker_naive 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring Ideal Algebra.Generators.Ring HasQuotient.Quotient CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id toGenerators naive SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Generators.ker	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective relation_mem_ker
naive_relation 📖	mathematical	—	relation HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id naive	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
naive_relation_apply 📖	mathematical	—	relation HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id naive	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
naive_toGenerators 📖	mathematical	—	toGenerators HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id naive Algebra.Generators.naive	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
ofAlgEquiv_relation 📖	mathematical	—	relation ofAlgEquiv	—	—
ofAlgEquiv_toGenerators 📖	mathematical	—	toGenerators ofAlgEquiv Algebra.Generators.ofAlgEquiv	—	—
ofBijectiveAlgebraMap_dimension 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	dimension ofBijectiveAlgebraMap	—	Nat.card_eq_fintype_card Fintype.card_eq_zero PEmpty.instIsEmpty tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub
quotientEquiv_mk 📖	mathematical	—	DFunLike.coe AlgEquiv Algebra.Generators.Ring toGenerators Quotient MvPolynomial.commSemiring CommRing.toCommSemiring Ideal.Quotient.semiring MvPolynomial.instCommRingMvPolynomial Algebra.Generators.ker CommSemiring.toSemiring Ideal.instAlgebraQuotient Algebra.id Algebra.Generators.instRing AlgEquiv.instFunLike quotientEquiv RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike algebraMap	—	Ideal.instIsTwoSided_1
quotientEquiv_symm 📖	mathematical	—	DFunLike.coe AlgEquiv Algebra.Generators.Ring toGenerators Quotient MvPolynomial.commSemiring CommRing.toCommSemiring CommSemiring.toSemiring Ideal.Quotient.semiring MvPolynomial.instCommRingMvPolynomial Algebra.Generators.ker Algebra.Generators.instRing Ideal.instAlgebraQuotient Algebra.id AlgEquiv.instFunLike AlgEquiv.symm quotientEquiv RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Algebra.Generators.σ	—	—
reindex_toGenerators 📖	mathematical	—	toGenerators reindex Algebra.Generators.reindex	—	—
relation_comp_localizationAway_inl 📖	mathematical	Algebra.Generators.σ toGenerators NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Algebra.Generators.Ring MvPolynomial.instCommRingMvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	relation comp localizationAway MvPolynomial CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe AlgHom CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename MvPolynomial.X	—	MvPolynomial.C_mul_X_eq_monomial map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_eq_add_neg map_neg RingHomClass.toAddMonoidHomClass Finsupp.sum_single_add_single map_zero MonoidWithZeroHomClass.toZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.zero_mul Finsupp.mapDomain_single pow_one DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Finsupp.mapDomain_zero mul_one MvPolynomial.C_neg
relation_mem_ker 📖	mathematical	—	Algebra.Generators.Ring toGenerators Ideal CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.Generators.ker relation	—	span_range_relation_eq_ker Ideal.subset_span
span_range_relation_eq_ker 📖	mathematical	—	Ideal.span Algebra.Generators.Ring toGenerators CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring Set.range relation Algebra.Generators.ker	—	—
toGenerators_comp 📖	mathematical	—	toGenerators comp Algebra.Generators.comp	—	—

---

← Back to Index