Generators

📁 Source: Mathlib/RingTheory/Extension/Generators.lean

Statistics

Metric	Count
Definitions comp, equivAlgHom, id, toAlgHom, toExtensionHom, val, σ, algebra, baseChange, comp, defaultHom, extend, extendScalars, id, instInhabitedHom, instRing, ker, kerCompPreimage, localizationAway, naive, ofAlgEquiv, ofAlgHom, ofComp, ofSet, ofSurjective, ofSurjectiveAlgebraMap, reindex, self, toComp, toExtendScalars, toExtension, val, σ, σ', Generators, Generators, Generators	37
Theorems iff_exists_generators, aeval_val, algebraMap_toAlgHom, algebraMap_toAlgHom', comp_id, comp_val, equivAlgHom_apply_coe, equivAlgHom_symm_apply_val, ext, ext_iff, id_comp, id_val, toAlgHom_C, toAlgHom_X, toAlgHom_comp_apply, toAlgHom_id, toAlgHom_monomial, toExtensionHom_comp, toExtensionHom_id, toExtensionHom_toAlgHom_apply, toExtensionHom_toRingHom, aeval_val_eq_zero, aeval_val_surjective, aeval_val_σ, aeval_val_σ', algebraMap_apply, algebraMap_eq, algebraMap_surjective, baseChange_val, comp_val, comp_σ, defaultHom_val, extendScalars_val, extend_val_inl, extend_val_inr, finiteType, instIsScalarTowerRing, ker_comp_eq_sup, ker_eq_ker_aeval_val, ker_naive, ker_ofAlgEquiv, ker_ofAlgHom, localizationAway_val, localizationAway_σ, map_ofComp_ker, map_toComp_ker, naive_val, naive_σ, ofAlgEquiv_val, ofComp_kerCompPreimage, ofComp_toAlgHom_monomial_sumElim, ofComp_val, ofSurjective_val, reindex_val, self_algebra_algebraMap, self_algebra_smul, self_val, self_σ, toAlgHom_ofComp_localizationAway, toAlgHom_ofComp_rename, toAlgHom_ofComp_surjective, toComp_toAlgHom, toComp_toAlgHom_monomial, toComp_val, toExtendScalars_val, toExtension_Ring, toExtension_algebra₁, toExtension_algebra₂, toExtension_commRing, toExtension_σ, σ_injective, σ_smul	72
Total	109

Algebra.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_generators 📖	mathematical	—	Algebra.FiniteType CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Generators	—	iff_quotient_mvPolynomial'' MvPolynomial.aeval_unique Algebra.Generators.finiteType Finite.of_fintype

Algebra.Generators

Definitions

Name	Category	Theorems
algebra 📖	CompOp	11 math math: StandardEtalePresentation.toPresentation_algebra_smul, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, algebraMap_eq, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, self_algebra_smul, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, self_algebra_algebraMap, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul
baseChange 📖	CompOp	2 math math: baseChange_val, Algebra.Presentation.baseChange_toGenerators
comp 📖	CompOp	42 math math: toAlgHom_ofComp_localizationAway, compLocalizationAwayAlgHom_toAlgHom_toComp, liftBaseChange_injective_of_isLocalizationAway, map_toComp_ker, ofComp_val, toComp_val, compLocalizationAwayAlgHom_X_inl, map_ofComp_ker, H1Cotangent.exact_map_δ, CotangentSpace.compEquiv_symm_zero, toAlgHom_ofComp_surjective, comp_val, map_comp_cotangentCompAwaySec, Cotangent.surjective_map_ofComp, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, cotangentCompLocalizationAwayEquiv_symm_comp_inl, Algebra.Presentation.comp_relation, Algebra.Presentation.toGenerators_comp, snd_comp_cotangentCompLocalizationAwayEquiv, H1Cotangent.δAux_ofComp, cotangentCompAwaySec_apply, toAlgHom_ofComp_rename, comp_localizationAway_ker, Cotangent.exact, toComp_toAlgHom, toComp_toAlgHom_monomial, CotangentSpace.exact, ofComp_kerCompPreimage, CotangentSpace.compEquiv_symm_inr, ker_comp_eq_sup, ofComp_toAlgHom_monomial_sumElim, snd_cotangentCompLocalizationAwayEquiv, CotangentSpace.map_toComp_injective, compLocalizationAwayAlgHom_relation_eq_zero, cotangentCompLocalizationAwayEquiv_symm_inl, cotangentCompLocalizationAwayEquiv_symm_inr, CotangentSpace.fst_compEquiv_apply, comp_σ, CotangentSpace.map_ofComp_surjective, H1Cotangent.map_comp_cotangentComplex_baseChange, CotangentSpace.fst_compEquiv, Algebra.PreSubmersivePresentation.toGenerators_comp
defaultHom 📖	CompOp	2 math math: defaultHom_val, H1Cotangent.equiv_apply
extend 📖	CompOp	2 math math: extend_val_inr, extend_val_inl
extendScalars 📖	CompOp	2 math math: toExtendScalars_val, extendScalars_val
id 📖	CompOp	—
instInhabitedHom 📖	CompOp	—
instRing 📖	CompOp	12 math math: H1Cotangent.δAux_mul, cotangentSpaceBasis_apply, algebraMap_surjective, Algebra.Presentation.quotientEquiv_symm, toExtension_algebra₂, algebraMap_apply, H1Cotangent.δAux_toAlgHom, instIsScalarTowerRing, toAlgHom_ofComp_rename, σ_smul, Algebra.Presentation.quotientEquiv_mk, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
ker 📖	CompOp	27 math math: Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.Presentation.quotientEquiv_symm, map_toComp_ker, compLocalizationAwayAlgHom_X_inl, map_ofComp_ker, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Algebra.Presentation.span_range_relation_eq_ker, ker_localizationAway, Algebra.Presentation.fg_ker, Algebra.Presentation.relation_mem_ker, comp_localizationAway_ker, ker_ofAlgEquiv, ofComp_kerCompPreimage, ker_comp_eq_sup, ker_eq_ker_aeval_val, ker_ofAlgHom, cotangentRestrict_mk, H1Cotangent.δ_eq_δAux, compLocalizationAwayAlgHom_relation_eq_zero, fg_ker_of_finitePresentation, Algebra.Presentation.quotientEquiv_mk, Algebra.Presentation.instFinitePresentationQuotientOfFinite, ker_naive, Algebra.Presentation.mem_ker_naive, C_mul_X_sub_one_mem_ker
kerCompPreimage 📖	CompOp	1 math math: ofComp_kerCompPreimage
localizationAway 📖	CompOp	22 math math: toAlgHom_ofComp_localizationAway, Algebra.Presentation.localizationAway_relation, compLocalizationAwayAlgHom_toAlgHom_toComp, liftBaseChange_injective_of_isLocalizationAway, compLocalizationAwayAlgHom_X_inl, map_comp_cotangentCompAwaySec, localizationAway_σ, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, cotangentCompLocalizationAwayEquiv_symm_comp_inl, snd_comp_cotangentCompLocalizationAwayEquiv, cotangentCompAwaySec_apply, ker_localizationAway, comp_localizationAway_ker, cMulXSubOneCotangent_eq, localizationAway_val, snd_cotangentCompLocalizationAwayEquiv, compLocalizationAwayAlgHom_relation_eq_zero, cotangentCompLocalizationAwayEquiv_symm_inl, cotangentCompLocalizationAwayEquiv_symm_inr, Algebra.instFreeCotangentToExtensionUnitLocalizationAway, basisCotangentAway_apply, C_mul_X_sub_one_mem_ker
naive 📖	CompOp	4 math math: Algebra.Presentation.naive_toGenerators, naive_val, naive_σ, ker_naive
ofAlgEquiv 📖	CompOp	3 math math: ker_ofAlgEquiv, Algebra.Presentation.ofAlgEquiv_toGenerators, ofAlgEquiv_val
ofAlgHom 📖	CompOp	2 math math: ker_ofAlgHom, StandardEtalePresentation.toPresentation_relation
ofComp 📖	CompOp	20 math math: toAlgHom_ofComp_localizationAway, map_toComp_ker, ofComp_val, map_ofComp_ker, H1Cotangent.exact_map_δ, toAlgHom_ofComp_surjective, map_comp_cotangentCompAwaySec, Cotangent.surjective_map_ofComp, snd_comp_cotangentCompLocalizationAwayEquiv, H1Cotangent.δAux_ofComp, toAlgHom_ofComp_rename, Cotangent.exact, CotangentSpace.exact, ofComp_kerCompPreimage, ker_comp_eq_sup, ofComp_toAlgHom_monomial_sumElim, snd_cotangentCompLocalizationAwayEquiv, CotangentSpace.fst_compEquiv_apply, CotangentSpace.map_ofComp_surjective, CotangentSpace.fst_compEquiv
ofSet 📖	CompOp	—
ofSurjective 📖	CompOp	1 math math: ofSurjective_val
ofSurjectiveAlgebraMap 📖	CompOp	—
reindex 📖	CompOp	2 math math: reindex_val, Algebra.Presentation.reindex_toGenerators
self 📖	CompOp	11 math math: self_val, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, self_σ, self_algebra_smul, Algebra.H1Cotangent.isLocalizedModule, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, Algebra.H1Cotangent.exact_map_δ, self_algebra_algebraMap, Algebra.smoothLocus_eq_compl_support_inter, Algebra.H1Cotangent.exact_δ_mapBaseChange, Algebra.etaleLocus_eq_compl_support
toComp 📖	CompOp	16 math math: compLocalizationAwayAlgHom_toAlgHom_toComp, liftBaseChange_injective_of_isLocalizationAway, map_toComp_ker, toComp_val, CotangentSpace.compEquiv_symm_zero, cotangentCompLocalizationAwayEquiv_symm_comp_inl, comp_localizationAway_ker, Cotangent.exact, toComp_toAlgHom, toComp_toAlgHom_monomial, CotangentSpace.exact, CotangentSpace.compEquiv_symm_inr, ker_comp_eq_sup, CotangentSpace.map_toComp_injective, cotangentCompLocalizationAwayEquiv_symm_inl, H1Cotangent.map_comp_cotangentComplex_baseChange
toExtendScalars 📖	CompOp	1 math math: toExtendScalars_val
toExtension 📖	CompOp	79 math math: Algebra.SubmersivePresentation.cotangentComplexAux_injective, Algebra.Presentation.differentials.comm₁₂_single, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, toExtension_σ, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.Presentation.differentials.hom₁_single, exists_presentation_of_basis_cotangent, liftBaseChange_injective_of_isLocalizationAway, cotangentSpaceBasis_repr_one_tmul, Hom.toExtensionHom_toAlgHom_apply, toExtension_algebra₂, exists_presentation_of_free_cotangent, H1Cotangent.exact_map_δ, CotangentSpace.compEquiv_symm_zero, cotangentSpaceBasis_repr_tmul, H1Cotangent.δAux_toAlgHom, map_comp_cotangentCompAwaySec, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Hom.toExtensionHom_id, Algebra.Presentation.differentials.surjective_hom₁, Cotangent.surjective_map_ofComp, H1Cotangent.exact_δ_map, cotangentCompLocalizationAwayEquiv_symm_comp_inl, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, snd_comp_cotangentCompLocalizationAwayEquiv, cotangentRestrict_bijective_of_isCompl, H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', cotangentCompAwaySec_apply, Hom.toExtensionHom_toRingHom, Algebra.SubmersivePresentation.subsingleton_h1Cotangent, Cotangent.exact, cMulXSubOneCotangent_eq, toKaehler_tmul_D, Algebra.Presentation.differentials.comm₁₂, H1Cotangent.δ_eq, H1Cotangent.exact_map_δ', disjoint_ker_toKaehler_of_linearIndependent, CotangentSpace.exact, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, Hom.toExtensionHom_comp, repr_CotangentSpaceMap, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, toKaehler_cotangentSpaceBasis, CotangentSpace.compEquiv_symm_inr, toExtension_algebra₁, Algebra.H1Cotangent.isLocalizedModule, cotangentRestrict_mk, cotangentRestrict_bijective_of_basis_kaehlerDifferential, H1Cotangent.δ_eq_δAux, snd_cotangentCompLocalizationAwayEquiv, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, CotangentSpace.map_toComp_injective, toExtension_Ring, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.H1Cotangent.exact_map_δ, H1Cotangent.δ_comp_equiv, cotangentCompLocalizationAwayEquiv_symm_inl, cotangentCompLocalizationAwayEquiv_symm_inr, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, instFreeCotangentSpaceToExtension, Algebra.SubmersivePresentation.free_cotangent, CotangentSpace.fst_compEquiv_apply, Algebra.smoothLocus_eq_compl_support_inter, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.instFreeCotangentToExtensionUnitLocalizationAway, Algebra.SubmersivePresentation.basisCotangent_apply, basisCotangentAway_apply, CotangentSpace.map_ofComp_surjective, H1Cotangent.map_comp_cotangentComplex_baseChange, CotangentSpace.fst_compEquiv, H1Cotangent.equiv_apply, Algebra.H1Cotangent.exact_δ_mapBaseChange, Algebra.SubmersivePresentation.cotangentEquiv_apply, H1Cotangent.δ_map, Algebra.etaleLocus_eq_compl_support, toExtension_commRing
val 📖	CompOp	56 math math: baseChange_val, aeval_val_surjective, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, self_val, defaultHom_val, exists_presentation_of_basis_cotangent, cotangentSpaceBasis_repr_one_tmul, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, ofComp_val, exists_presentation_of_free_cotangent, naive_val, algebraMap_apply, algebraMap_eq, Hom.aeval_val, Algebra.Presentation.comp_aeval_relation_inl, extend_val_inr, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, H1Cotangent.δAux_monomial, Hom.algebraMap_toAlgHom', cotangentSpaceBasis_repr_tmul, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, comp_val, Algebra.Presentation.aeval_val_relation, Algebra.Presentation.differentials.comm₂₃', Algebra.PreSubmersivePresentation.aevalDifferential_single, aeval_val_σ, Algebra.SubmersivePresentation.ofSubsingleton_val, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, toKaehler_tmul_D, extendScalars_val, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, Algebra.Presentation.aeval_val_relationOfHasCoeffs, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, repr_CotangentSpaceMap, reindex_val, toKaehler_cotangentSpaceBasis, localizationAway_val, Algebra.SubmersivePresentation.basisKaehler_apply, ofComp_toAlgHom_monomial_sumElim, aeval_val_eq_zero, StandardEtalePresentation.aeval_val_equivMvPolynomial, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, ker_eq_ker_aeval_val, cotangentRestrict_mk, aeval_val_σ', StandardEtalePresentation.toPresentation_val, ofAlgEquiv_val, MvPolynomial.universalFactorizationMapPresentation_val, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Hom.algebraMap_toAlgHom, ofSurjective_val, extend_val_inl, Algebra.SubmersivePresentation.basisDeriv_apply, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val
σ 📖	CompOp	19 math math: toAlgHom_ofComp_localizationAway, toExtension_σ, defaultHom_val, compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.Presentation.quotientEquiv_symm, compLocalizationAwayAlgHom_X_inl, Algebra.SubmersivePresentation.jacobianRelations_spec, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, localizationAway_σ, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, σ_smul, σ_injective, aeval_val_σ, self_σ, Algebra.Presentation.relation_comp_localizationAway_inl, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, naive_σ, compLocalizationAwayAlgHom_relation_eq_zero, comp_σ
σ' 📖	CompOp	5 math math: Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', StandardEtalePresentation.toPresentation_σ', aeval_val_σ', Algebra.SubmersivePresentation.ofSubsingleton_σ', MvPolynomial.universalFactorizationMapPresentation_σ'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_val_eq_zero 📖	mathematical	Ring Ideal AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddMonoid Nat.instAddMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	algebraMap_apply
aeval_val_surjective 📖	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 MvPolynomial.aeval val	—	aeval_val_σ
aeval_val_σ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val σ	—	aeval_val_σ'
aeval_val_σ' 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val σ'	—	—
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.instFunLike algebraMap instRing AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val	—	AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMap_eq
algebraMap_eq 📖	mathematical	—	algebraMap MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CommSemiring.toSemiring algebra RingHomClass.toRingHom AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass MvPolynomial.aeval val	—	—
algebraMap_surjective 📖	mathematical	—	Ring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.instFunLike algebraMap instRing	—	aeval_val_σ algebraMap_apply
baseChange_val 📖	mathematical	—	val 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 TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Algebra.to_smulCommClass
comp_val 📖	mathematical	—	val comp DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	—
comp_σ 📖	mathematical	—	σ comp Finsupp.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial CommRing.toCommSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.rename LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike MvPolynomial.monomial Finsupp.mapDomain Nat.instAddCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
defaultHom_val 📖	mathematical	—	Hom.val defaultHom Ring σ DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap val	—	—
extendScalars_val 📖	mathematical	—	val extendScalars	—	—
extend_val_inl 📖	mathematical	—	val extend	—	—
extend_val_inr 📖	mathematical	—	val extend	—	—
finiteType 📖	mathematical	—	Algebra.FiniteType CommRing.toCommSemiring CommSemiring.toSemiring	—	Algebra.FiniteType.of_surjective Algebra.FiniteType.instMvPolynomialOfFinite Module.Finite.finiteType Module.Finite.self instIsScalarTowerRing IsScalarTower.left algebraMap_surjective
instIsScalarTowerRing 📖	mathematical	—	IsScalarTower Ring Algebra.toSMul CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid instRing	—	IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap_of_tower AddMonoidAlgebra.isScalarTower IsScalarTower.right algebraMap_eq
ker_comp_eq_sup 📖	mathematical	—	ker comp Ideal Ring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddMonoid Nat.instAddMonoid SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.id Ideal.map AlgHom AddMonoidAlgebra.algebra AlgHom.funLike Hom.toAlgHom toComp Ideal.comap ofComp AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_ofComp_ker Ideal.comap_map_of_surjective toAlgHom_ofComp_surjective sup_assoc map_toComp_ker RingHom.ker_eq_comap_bot le_antisymm le_trans le_sup_right le_sup_left sup_of_le_left ker_eq_ker_aeval_val RingHom.mem_ker Algebra.algebraMap_self_apply Hom.algebraMap_toAlgHom IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass
ker_eq_ker_aeval_val 📖	mathematical	—	ker RingHom.ker MvPolynomial CommRing.toCommSemiring AlgHom AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass MvPolynomial.aeval val	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ker.congr_simp algebraMap_eq
ker_naive 📖	mathematical	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring HasQuotient.Quotient Ideal Ring.toSemiring AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.instFunLike	ker HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient_1 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Ideal.Quotient.commRing Ideal.instAlgebraQuotient AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid naive	—	Ideal.instIsTwoSided_1 Ideal.mk_ker
ker_ofAlgEquiv 📖	mathematical	—	ker ofAlgEquiv	—	AlgHomClass.toRingHomClass AlgHom.algHomClass ker_eq_ker_aeval_val ofAlgEquiv_val AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgHom.coe_coe MvPolynomial.comp_aeval AlgHom.comap_ker RingHom.instRingHomClass RingHom.ker_coe_toRingHom AlgHomClass.toRingHom_toAlgHom AlgHom.ker_coe_equiv RingHom.ker_eq_comap_bot
ker_ofAlgHom 📖	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	ker ofAlgHom RingHom.ker MvPolynomial CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid RingHom.instFunLike RingHom.instRingHomClass AlgHom.toRingHom AddMonoidAlgebra.algebra Algebra.id	—	RingHom.instRingHomClass MvPolynomial.ringHom_ext algebraMap_apply MvPolynomial.algHom_C MvPolynomial.aeval_X
localizationAway_val 📖	mathematical	—	val localizationAway IsLocalization.Away.invSelf CommRing.toCommSemiring	—	—
localizationAway_σ 📖	mathematical	—	σ localizationAway MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C IsLocalization.Away.sec Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp.instAddMonoid MvPolynomial.X	—	—
map_ofComp_ker 📖	mathematical	—	Ideal.map Ring comp AlgHom CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp ker	—	Ideal.ext Ideal.mem_map_iff_of_surjective AlgHomClass.toRingHomClass AlgHom.algHomClass toAlgHom_ofComp_surjective ker_eq_ker_aeval_val Hom.algebraMap_toAlgHom IsScalarTower.right Algebra.algebraMap_self_apply ofComp_kerCompPreimage
map_toComp_ker 📖	mathematical	—	Ideal.map Ring comp AlgHom CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom toComp ker RingHom.ker AlgHomClass.toRingHomClass AlgHom.algHomClass ofComp	—	le_antisymm AlgHomClass.toRingHomClass AlgHom.algHomClass Ideal.map_le_iff_le_comap AddMonoidAlgebra.isScalarTower instIsScalarTowerRing IsScalarTower.left MvPolynomial.algHom_ext Hom.toAlgHom_X algebraMap_apply MvPolynomial.aeval_X IsScalarTower.algebraMap_apply IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.sum_fiberwise_of_maps_to Finset.mem_image_of_mem sum_mem Submodule.addSubmonoidClass map_sum RingHomClass.toAddMonoidHomClass Finset.mul_sum Finset.sum_congr toComp_toAlgHom_monomial MvPolynomial.monomial_mul map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass add_zero zero_add one_mul Finset.mem_filter Ideal.mul_mem_left Ideal.mem_map_of_mem ker_eq_ker_aeval_val DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass MvPolynomial.coeff_zero Set.compl_subset_compl AddEquiv.surjective Finset.coe_map Set.image_congr EquivLike.toEmbeddingLike AddEquiv.symm_apply_apply MvPolynomial.monomial_zero Finset.sum_filter finsum_eq_sum_of_support_subset MvPolynomial.induction_on' ofComp_toAlgHom_monomial_sumElim MvPolynomial.coeff_monomial AddEquiv.injective AddEquiv.apply_symm_apply AddMonoidHomClass.toZeroHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_ite_eq ite_and MvPolynomial.coeff_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass ite_add_zero finsum_add_distrib Set.Finite.subset Finset.finite_toSet Finset.sum_map MvPolynomial.support_sum_monomial_coeff
naive_val 📖	mathematical	—	val HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient_1 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Ideal.Quotient.commRing Ideal.instAlgebraQuotient AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid naive DFunLike.coe RingHom Ring.toSemiring AddMonoidAlgebra.ring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring RingHom.instFunLike MvPolynomial.X	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
naive_σ 📖	mathematical	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring HasQuotient.Quotient Ideal Ring.toSemiring AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.instFunLike	σ HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient_1 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Ideal.Quotient.commRing Ideal.instAlgebraQuotient AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid naive	—	Ideal.instIsTwoSided_1
ofAlgEquiv_val 📖	mathematical	—	val ofAlgEquiv DFunLike.coe AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike	—	—
ofComp_kerCompPreimage 📖	mathematical	—	DFunLike.coe AlgHom Ring comp CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker kerCompPreimage	—	MvPolynomial.support_sum_monomial_coeff kerCompPreimage.eq_1 map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Finsupp.sum.eq_1 Finset.sum_congr map_mul NonUnitalAlgSemiHomClass.toMulHomClass Hom.toAlgHom_monomial one_smul Sum.inl_injective MvPolynomial.rename.eq_1 AlgHom.comp_apply MvPolynomial.comp_aeval Hom.toAlgHom_X MvPolynomial.monomial_eq MvPolynomial.aeval_def IsScalarTower.algebraMap_eq AddMonoidAlgebra.isScalarTower IsScalarTower.right MvPolynomial.algebraMap_eq MvPolynomial.coe_eval₂Hom MvPolynomial.map_aeval aeval_val_σ
ofComp_toAlgHom_monomial_sumElim 📖	mathematical	—	DFunLike.coe AlgHom Ring comp CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp LinearMap RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike MvPolynomial.monomial Finsupp.sumElim MvPolynomial.aeval val	—	Hom.toAlgHom_monomial MvPolynomial.monomial_eq MvPolynomial.aeval_monomial Finsupp.prod_sumElim MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.smul_def MvPolynomial.C_mul mul_assoc mul_comm
ofComp_val 📖	mathematical	—	Hom.val comp Algebra.id CommRing.toCommSemiring ofComp Ring MvPolynomial.X DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.C val	—	—
ofSurjective_val 📖	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 MvPolynomial.aeval	val ofSurjective	—	—
reindex_val 📖	mathematical	—	val reindex DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
self_algebra_algebraMap 📖	mathematical	—	Algebra.algebraMap MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CommSemiring.toSemiring algebra self AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id MvPolynomial.aeval	—	—
self_algebra_smul 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring Algebra.toSMul AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CommSemiring.toSemiring algebra self Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id MvPolynomial.aeval	—	—
self_val 📖	mathematical	—	val self	—	—
self_σ 📖	mathematical	—	σ self MvPolynomial.X CommRing.toCommSemiring	—	—
toAlgHom_ofComp_localizationAway 📖	mathematical	—	DFunLike.coe AlgHom Ring comp localizationAway CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp MvPolynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring CommRing.toRing AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass MvPolynomial.rename σ MvPolynomial.X AddMonoidAlgebra.zero Finsupp.instZero RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass MvPolynomial.aeval_rename MvPolynomial.aeval_C_comp_left aeval_val_σ MvPolynomial.aeval_X map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass
toAlgHom_ofComp_rename 📖	mathematical	—	DFunLike.coe AlgHom Ring comp CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp MvPolynomial MvPolynomial.rename RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike MvPolynomial.C AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid algebraMap instRing	—	AddMonoidAlgebra.isScalarTower IsScalarTower.right instIsScalarTowerRing IsScalarTower.left MvPolynomial.algHom_ext MvPolynomial.ext MvPolynomial.rename_X Hom.toAlgHom_X algebraMap_apply MvPolynomial.aeval_X DFunLike.congr_fun
toAlgHom_ofComp_surjective 📖	mathematical	—	Ring comp DFunLike.coe AlgHom CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp	—	MvPolynomial.induction_on MvPolynomial.aeval_rename AddMonoidAlgebra.isScalarTower IsScalarTower.right aeval_val_σ map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass MvPolynomial.aeval_X
toComp_toAlgHom 📖	mathematical	—	Hom.toAlgHom comp Algebra.id CommRing.toCommSemiring toComp MvPolynomial.rename	—	—
toComp_toAlgHom_monomial 📖	mathematical	—	DFunLike.coe AlgHom Ring comp CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Hom.toAlgHom toComp LinearMap RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike MvPolynomial.monomial Finsupp.sumElim Finsupp.instZero	—	Finsupp.ext Finsupp.mapDomain_notin_range Finsupp.mapDomain_apply Sum.inr_injective MvPolynomial.rename_monomial
toComp_val 📖	mathematical	—	Hom.val comp toComp MvPolynomial.X CommRing.toCommSemiring	—	—
toExtendScalars_val 📖	mathematical	—	Hom.val extendScalars Algebra.id CommRing.toCommSemiring toExtendScalars MvPolynomial.X	—	—
toExtension_Ring 📖	mathematical	—	Algebra.Extension.Ring toExtension Ring	—	—
toExtension_algebra₁ 📖	mathematical	—	Algebra.Extension.algebra₁ toExtension AddMonoidAlgebra.algebra Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Nat.instAddCommMonoid	—	—
toExtension_algebra₂ 📖	mathematical	—	Algebra.Extension.algebra₂ toExtension instRing	—	—
toExtension_commRing 📖	mathematical	—	Algebra.Extension.commRing toExtension AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid	—	—
toExtension_σ 📖	mathematical	—	Algebra.Extension.σ toExtension σ	—	—
σ_injective 📖	mathematical	—	Ring σ	—	aeval_val_σ
σ_smul 📖	mathematical	—	Ring Algebra.toSMul AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid CommSemiring.toSemiring instRing σ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Algebra.smul_def algebraMap_apply aeval_val_σ

Algebra.Generators.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	5 math math: comp_id, toAlgHom_comp_apply, toExtensionHom_comp, comp_val, id_comp
equivAlgHom 📖	CompOp	2 math math: equivAlgHom_symm_apply_val, equivAlgHom_apply_coe
id 📖	CompOp	5 math math: id_val, comp_id, toExtensionHom_id, toAlgHom_id, id_comp
toAlgHom 📖	CompOp	24 math math: Algebra.Generators.toAlgHom_ofComp_localizationAway, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.Generators.map_toComp_ker, toExtensionHom_toAlgHom_apply, Algebra.Generators.map_ofComp_ker, Algebra.Generators.toAlgHom_ofComp_surjective, algebraMap_toAlgHom', Algebra.Generators.H1Cotangent.δAux_toAlgHom, toAlgHom_X, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Generators.toAlgHom_ofComp_rename, toExtensionHom_toRingHom, Algebra.Generators.comp_localizationAway_ker, Algebra.Generators.toComp_toAlgHom, toAlgHom_C, toAlgHom_comp_apply, Algebra.Generators.toComp_toAlgHom_monomial, Algebra.Generators.ofComp_kerCompPreimage, Algebra.Generators.ker_comp_eq_sup, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, toAlgHom_id, toAlgHom_monomial, algebraMap_toAlgHom, equivAlgHom_apply_coe
toExtensionHom 📖	CompOp	25 math math: Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, toExtensionHom_toAlgHom_apply, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.map_comp_cotangentCompAwaySec, toExtensionHom_id, Algebra.Generators.Cotangent.surjective_map_ofComp, Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl, Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv, toExtensionHom_toRingHom, Algebra.Generators.Cotangent.exact, Algebra.Generators.H1Cotangent.exact_map_δ', Algebra.Generators.CotangentSpace.exact, toExtensionHom_comp, Algebra.Generators.repr_CotangentSpaceMap, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv, Algebra.Generators.CotangentSpace.map_toComp_injective, Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.Generators.H1Cotangent.δ_map
val 📖	CompOp	13 math math: Algebra.Generators.defaultHom_val, Algebra.Generators.ofComp_val, Algebra.Generators.toComp_val, id_val, aeval_val, Algebra.Generators.H1Cotangent.δAux_toAlgHom, ext_iff, toAlgHom_X, Algebra.Generators.toExtendScalars_val, Algebra.Generators.repr_CotangentSpaceMap, equivAlgHom_symm_apply_val, comp_val, toAlgHom_monomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_val 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val val RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	—
algebraMap_toAlgHom 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Generators.Ring toAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	AddMonoidAlgebra.isScalarTower IsScalarTower.right MvPolynomial.algHom_ext MvPolynomial.aeval_X aeval_val DFunLike.congr_fun
algebraMap_toAlgHom' 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Generators.Ring toAlgHom	—	algebraMap_toAlgHom IsScalarTower.right
comp_id 📖	mathematical	—	comp Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule id	—	ext IsScalarTower.left MvPolynomial.ext MvPolynomial.aeval_X
comp_val 📖	mathematical	—	val comp DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring Algebra.Generators.Ring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgHom.funLike MvPolynomial.aeval	—	—
equivAlgHom_apply_coe 📖	mathematical	—	AlgHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id DFunLike.coe Equiv Algebra.Generators.Hom EquivLike.toFunLike Equiv.instEquivLike equivAlgHom toAlgHom	—	—
equivAlgHom_symm_apply_val 📖	mathematical	—	val DFunLike.coe Equiv AlgHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Algebra.Generators.Hom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivAlgHom AlgHom.funLike MvPolynomial.X	—	—
ext 📖	—	val	—	—	—
ext_iff 📖	mathematical	—	val	—	ext
id_comp 📖	mathematical	—	comp Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule IsScalarTower.right id	—	ext IsScalarTower.left IsScalarTower.right MvPolynomial.ext MvPolynomial.aeval_X_left
id_val 📖	mathematical	—	val Algebra.id CommRing.toCommSemiring id MvPolynomial.X	—	—
toAlgHom_C 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike toAlgHom RingHom MvPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike MvPolynomial.C algebraMap	—	MvPolynomial.aeval_C
toAlgHom_X 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike toAlgHom MvPolynomial.X val	—	MvPolynomial.aeval_X
toAlgHom_comp_apply 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike toAlgHom comp	—	MvPolynomial.induction_on AlgHom.map_algebraMap AddMonoidAlgebra.isScalarTower IsScalarTower.right IsScalarTower.left map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass toAlgHom_X
toAlgHom_id 📖	mathematical	—	toAlgHom Algebra.id CommRing.toCommSemiring id AlgHom.id Algebra.Generators.Ring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra	—	MvPolynomial.algHom_ext toAlgHom_X
toAlgHom_monomial 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike toAlgHom LinearMap RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike MvPolynomial.monomial Algebra.toSMul Finsupp.prod CommRing.toCommMonoid AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero val	—	toAlgHom.eq_1 MvPolynomial.aeval_monomial Algebra.smul_def
toExtensionHom_comp 📖	mathematical	—	toExtensionHom comp Algebra.Extension.Hom.comp Algebra.Generators.toExtension	—	Algebra.Extension.Hom.ext RingHom.ext toAlgHom_comp_apply
toExtensionHom_id 📖	mathematical	—	toExtensionHom Algebra.id CommRing.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule IsScalarTower.right id Algebra.Extension.Hom.id Algebra.Generators.toExtension	—	Algebra.Extension.Hom.ext IsScalarTower.left IsScalarTower.right RingHom.ext toAlgHom_id
toExtensionHom_toAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Extension.Ring Algebra.Generators.toExtension CommRing.toCommSemiring CommSemiring.toSemiring Algebra.Extension.commRing Algebra.Extension.instRingOfIsScalarTower Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike Algebra.Extension.Hom.toAlgHom toExtensionHom Algebra.Generators.Ring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra toAlgHom	—	IsScalarTower.left
toExtensionHom_toRingHom 📖	mathematical	—	Algebra.Extension.Hom.toRingHom Algebra.Generators.toExtension toExtensionHom AlgHom.toRingHom Algebra.Generators.Ring CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id toAlgHom	—	—

Algebra.Generators.Simps

Definitions

Name	Category	Theorems
σ 📖	CompOp	—

CartanMatrix

Definitions

Name	Category	Theorems
Generators 📖	CompData	—

IsFreeGroup

Definitions

Name	Category	Theorems
Generators 📖	CompOp	2 math math: toFreeGroup_symm_apply, toFreeGroup_apply

IsFreeGroupoid

Definitions

Name	Category	Theorems
Generators 📖	CompOp	2 math math: path_nonempty_of_hom, generators_connected

---

← Back to Index