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	36 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, Cotangent.surjective_map_ofComp, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Algebra.Presentation.comp_relation, Algebra.Presentation.toGenerators_comp, 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, CotangentSpace.map_toComp_injective, compLocalizationAwayAlgHom_relation_eq_zero, 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	13 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, H1Cotangent.equiv_apply, 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	16 math math: toAlgHom_ofComp_localizationAway, Algebra.Presentation.localizationAway_relation, compLocalizationAwayAlgHom_toAlgHom_toComp, liftBaseChange_injective_of_isLocalizationAway, compLocalizationAwayAlgHom_X_inl, localizationAway_σ, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, cotangentCompAwaySec_apply, ker_localizationAway, comp_localizationAway_ker, cMulXSubOneCotangent_eq, localizationAway_val, compLocalizationAwayAlgHom_relation_eq_zero, 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	17 math math: toAlgHom_ofComp_localizationAway, map_toComp_ker, ofComp_val, map_ofComp_ker, H1Cotangent.exact_map_δ, toAlgHom_ofComp_surjective, Cotangent.surjective_map_ofComp, H1Cotangent.δAux_ofComp, toAlgHom_ofComp_rename, Cotangent.exact, CotangentSpace.exact, ofComp_kerCompPreimage, ker_comp_eq_sup, ofComp_toAlgHom_monomial_sumElim, 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	70 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, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Hom.toExtensionHom_id, Algebra.Presentation.differentials.surjective_hom₁, Cotangent.surjective_map_ofComp, H1Cotangent.exact_δ_map, Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential, 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.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, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, CotangentSpace.map_toComp_injective, toExtension_Ring, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.H1Cotangent.exact_map_δ, H1Cotangent.δ_comp_equiv, 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	18 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.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 CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker	DFunLike.coe AlgHom MvPolynomial MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	algebraMap_apply
aeval_val_surjective 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring DFunLike.coe AlgHom CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val	—	aeval_val_σ
aeval_val_σ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val σ	—	aeval_val_σ'
aeval_val_σ' 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val σ'	—	—
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom Ring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap instRing AlgHom MvPolynomial MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval val	—	AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMap_eq
algebraMap_eq 📖	mathematical	—	algebraMap MvPolynomial CommRing.toCommSemiring MvPolynomial.commSemiring CommSemiring.toSemiring algebra RingHomClass.toRingHom AlgHom MvPolynomial.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 MvPolynomial.commSemiring CommRing.toCommSemiring 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 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe AlgHom MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename LinearMap RingHom.id Semiring.toModule MvPolynomial.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 CommSemiring.toSemiring MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra instRing	—	IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap_of_tower MvPolynomial.isScalarTower IsScalarTower.right algebraMap_eq
ker_comp_eq_sup 📖	mathematical	—	ker comp Ideal Ring CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Ideal.map AlgHom MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 CommRing.toRing MvPolynomial.instCommRingMvPolynomial Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	ker CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id 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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike	ker ofAlgHom RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass AlgHom.toRingHom	—	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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C IsLocalization.Away.sec Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPolynomial.X	—	—
map_ofComp_ker 📖	mathematical	—	Ideal.map Ring comp AlgHom CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id naive DFunLike.coe RingHom Ring.toSemiring 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 CommRing.toRing MvPolynomial.instCommRingMvPolynomial Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	σ CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id 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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp LinearMap RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MvPolynomial.module LinearMap.instFunLike MvPolynomial.monomial Finsupp.sumElim MulZeroClass.toZero Nat.instMulZeroClass 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 MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C val	—	—
ofSurjective_val 📖	mathematical	MvPolynomial CommRing.toCommSemiring DFunLike.coe AlgHom CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 MvPolynomial.commSemiring CommSemiring.toSemiring algebra self AlgHom.toRingHom MvPolynomial.algebra Algebra.id MvPolynomial.aeval	—	—
self_algebra_smul 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring Algebra.toSMul MvPolynomial.commSemiring CommSemiring.toSemiring algebra self Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike AlgHom.toRingHom MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp 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 MvPolynomial.rename σ MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne RingHom Semiring.toNonAssocSemiring 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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp MvPolynomial MvPolynomial.rename RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.C algebraMap instRing	—	MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike Hom.toAlgHom ofComp	—	MvPolynomial.induction_on MvPolynomial.aeval_rename MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike Hom.toAlgHom toComp LinearMap RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MvPolynomial.module LinearMap.instFunLike MvPolynomial.monomial Finsupp.sumElim MulZeroClass.toZero Nat.instMulZeroClass Finsupp 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 MvPolynomial.algebra CommRing.toCommSemiring Algebra.id	—	—
toExtension_algebra₂ 📖	mathematical	—	Algebra.Extension.algebra₂ toExtension instRing	—	—
toExtension_commRing 📖	mathematical	—	Algebra.Extension.commRing toExtension MvPolynomial.instCommRingMvPolynomial	—	—
toExtension_σ 📖	mathematical	—	Algebra.Extension.σ toExtension σ	—	—
σ_injective 📖	mathematical	—	Ring σ	—	aeval_val_σ
σ_smul 📖	mathematical	—	Ring Algebra.toSMul MvPolynomial.commSemiring CommRing.toCommSemiring 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	20 math math: Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, toExtensionHom_toAlgHom_apply, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, toExtensionHom_id, Algebra.Generators.Cotangent.surjective_map_ofComp, 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.CotangentSpace.map_toComp_injective, 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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Generators.Ring toAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	MvPolynomial.isScalarTower IsScalarTower.right MvPolynomial.algHom_ext MvPolynomial.aeval_X aeval_val DFunLike.congr_fun
algebraMap_toAlgHom' 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval	—	—
equivAlgHom_apply_coe 📖	mathematical	—	AlgHom Algebra.Generators.Ring CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike toAlgHom RingHom MvPolynomial Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.C algebraMap	—	MvPolynomial.aeval_C
toAlgHom_X 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike toAlgHom MvPolynomial.X val	—	MvPolynomial.aeval_X
toAlgHom_comp_apply 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike toAlgHom comp	—	MvPolynomial.induction_on AlgHom.map_algebraMap MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra	—	MvPolynomial.algHom_ext toAlgHom_X
toAlgHom_monomial 📖	mathematical	—	DFunLike.coe AlgHom Algebra.Generators.Ring CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike toAlgHom LinearMap RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MvPolynomial.module LinearMap.instFunLike MvPolynomial.monomial Algebra.toSMul Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommRing.toCommMonoid MvPolynomial.instCommRingMvPolynomial Monoid.toNatPow 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 MvPolynomial.commSemiring MvPolynomial.algebra toAlgHom	—	IsScalarTower.left
toExtensionHom_toRingHom 📖	mathematical	—	Algebra.Extension.Hom.toRingHom Algebra.Generators.toExtension toExtensionHom AlgHom.toRingHom Algebra.Generators.Ring CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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