Rename

📁 Source: Mathlib/Algebra/MvPolynomial/Rename.lean

Statistics

Metric	Count
Definitions killCompl, rename, renameEquiv	3
Theorems aeval_comp_rename, aeval_rename, coeff_rename_embDomain, coeff_rename_eq_zero, coeff_rename_mapDomain, coeff_rename_ne_zero, constantCoeff_rename, eval_rename, eval_rename_prod_mk, eval₂Hom_rename, eval₂_cast_comp, eval₂_rename, eval₂_rename_prod_mk, exists_fin_rename, exists_finset_rename, exists_finset_rename₂, killCompl_C, killCompl_comp_rename, killCompl_map, killCompl_rename_app, map_comp_rename, map_rename, renameEquiv_apply, renameEquiv_refl, renameEquiv_symm, renameEquiv_trans, rename_C, rename_X, rename_comp_rename, rename_eq, rename_eval₂, rename_id, rename_id_apply, rename_injective, rename_leftInverse, rename_monomial, rename_prod_mk_eval₂, rename_rename, rename_rightInverse, rename_surjective, support_rename_of_injective	41
Total	44

MvPolynomial

Definitions

Name	Category	Theorems
killCompl 📖	CompOp	4 math math: killCompl_comp_rename, killCompl_C, killCompl_rename_app, killCompl_map
rename 📖	CompOp	96 math math: join₁_rename, exists_finset_rename, rename_rename, Algebra.Generators.toAlgHom_ofComp_localizationAway, map_comp_rename, prime_rename_iff, constantCoeff_rename, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, CommRingCat.free_map_coe, killCompl_comp_rename, eval_rename_prod_mk, rename_msymm, rename_id_apply, pderiv_rename, Algebra.Presentation.comp_relation_inr, map_rename, sumAlgEquiv_comp_rename_inr, rename_psum, totalDegree_rename_le, Polynomial.toMvPolynomial_eq_rename_comp, support_rename_of_injective, degreeOf_rename_of_injective, exists_rename_eq_of_vars_subset_range, coeff_rename_embDomain, rename_comp_expand, rename_esymm, comap_rename, WittVector.mul_polyOfInterest_aux4, rename_eval₂, eval₂Hom_rename, sumAlgEquiv_comp_rename_inl, exists_fin_rename, renameEquiv_apply, eval₂_cast_comp, bind₁_rename, wittStructureRat_prop, degrees_rename, Algebra.Presentation.comp_relation, wittStructureRat_rec, coeff_rename_mapDomain, Algebra.Generators.toAlgHom_ofComp_rename, wittStructureRat_rec_aux, wittStructureInt_prop, Algebra.Generators.comp_localizationAway_ker, rename_monomial, aeval_id_rename, killCompl_rename_app, Algebra.Generators.toComp_toAlgHom, rename_comp_toMvPolynomial, rename_rightInverse, bind₁_comp_rename, eval₂_rename, IsSymmetric.rename, rename_bind₁, renameSymmetricSubalgebra_symm_apply_coe, bind₁_rename_expand_wittPolynomial, rename_injective, eval_rename, witt_structure_prop, IsHomogeneous.rename_isHomogeneous_iff, Algebra.Presentation.relation_comp_localizationAway_inl, rename_polynomial_aeval_X, exists_finset_rename₂, rename_prod_mk_eval₂, rename_C, IsHomogeneous.rename_isHomogeneous, WittVector.polyOfInterest_vars_eq, degrees_rename_of_injective, optionEquivLeft_symm_apply, vars_rename, rename_comp_bind₁, rename_X, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, finSuccEquiv_rename_finSuccEquiv, rename_expand, isSymmetric_rename, rename_comp_rename, aeval_comp_rename, eval₂_rename_prod_mk, rename_leftInverse, weightedTotalDegree_rename_of_injective, rename_toMvPolynomial, aeval_rename, degreeOf_eq_natDegree, coeff_rename_eq_zero, WittVector.mul_polyOfInterest_aux3, universalFactorizationMapPresentation_jacobiMatrix, wittStructureInt_rename, supported_eq_range_rename, rename_hsymm, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, Algebra.Generators.comp_σ, rename_eq, rename_surjective, renameSymmetricSubalgebra_apply_coe, rename_id
renameEquiv 📖	CompOp	5 math math: renameEquiv_trans, renameEquiv_apply, renameEquiv_refl, totalDegree_renameEquiv, renameEquiv_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_comp_rename 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id aeval rename	—	AlgHom.ext aeval_rename
aeval_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval rename	—	eval₂Hom_rename
coeff_rename_embDomain 📖	mathematical	—	coeff Finsupp.embDomain MulZeroClass.toZero Nat.instMulZeroClass DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename Function.Embedding Function.instFunLikeEmbedding	—	Finsupp.embDomain_eq_mapDomain coeff_rename_mapDomain Function.Embedding.injective
coeff_rename_eq_zero 📖	mathematical	coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe AlgHom MvPolynomial commSemiring algebra Algebra.id AlgHom.funLike rename	—	rename_eq notMem_support_iff Finsupp.mapDomain_support Finset.mem_image Finsupp.mem_support_iff
coeff_rename_mapDomain 📖	mathematical	—	coeff Finsupp.mapDomain Nat.instAddCommMonoid DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	induction_on' rename_monomial coeff_monomial Finsupp.mapDomain_injective map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass coeff_add
coeff_rename_ne_zero 📖	mathematical	—	Finsupp.mapDomain Nat.instAddCommMonoid	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq coeff_rename_eq_zero
constantCoeff_rename 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff AlgHom algebra Algebra.id AlgHom.funLike rename	—	induction_on rename_C constantCoeff_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_X NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass constantCoeff_X
eval_rename 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval AlgHom algebra Algebra.id AlgHom.funLike rename	—	eval₂_rename
eval_rename_prod_mk 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval AlgHom algebra Algebra.id AlgHom.funLike rename	—	—
eval₂Hom_rename 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom AlgHom algebra Algebra.id AlgHom.funLike rename	—	eval₂_rename
eval₂_cast_comp 📖	mathematical	—	eval₂ Int.instCommSemiring DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	eval₂_rename
eval₂_rename 📖	mathematical	—	eval₂ DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	induction_on algHom_C eval₂_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass eval₂_add map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_X eval₂_mul eval₂_X
eval₂_rename_prod_mk 📖	mathematical	—	eval₂ DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	induction_on algHom_C eval₂_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass eval₂_add map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_X eval₂_mul eval₂_X
exists_fin_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	exists_finset_rename Subtype.val_injective Equiv.injective rename_rename Equiv.symm_apply_apply
exists_finset_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial Finset Finset.instMembership CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	induction_on rename_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass rename_rename Finset.mem_insert_self map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_X
exists_finset_rename₂ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial Finset SetLike.instMembership Finset.instSetLike CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	exists_finset_rename Finset.subset_union_left Finset.subset_union_right rename_rename
killCompl_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike killCompl RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	algHom_C
killCompl_comp_rename 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id killCompl rename AlgHom.id	—	algHom_ext rename.eq_1 killCompl.eq_1 aeval_X Equiv.ofInjective_symm_apply
killCompl_map 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike killCompl RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map	—	AlgHomClass.toRingHomClass AlgHom.algHomClass ringHom_ext' RingHom.ext ext map_C algHom_C map_X aeval_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
killCompl_rename_app 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike killCompl rename	—	AlgHom.congr_fun killCompl_comp_rename
map_comp_rename 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring map AlgHom.toRingHom algebra Algebra.id rename	—	RingHom.ext map_rename
map_rename 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map AlgHom algebra Algebra.id AlgHom.funLike rename	—	induction_on rename_C map_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_X NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_X
renameEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgEquiv.instFunLike renameEquiv AlgHom AlgHom.funLike rename Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
renameEquiv_refl 📖	mathematical	—	renameEquiv Equiv.refl AlgEquiv.refl MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id	—	AlgEquiv.ext rename_id
renameEquiv_symm 📖	mathematical	—	AlgEquiv.symm MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id renameEquiv Equiv.symm	—	—
renameEquiv_trans 📖	mathematical	—	AlgEquiv.trans MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id renameEquiv Equiv.trans	—	AlgEquiv.ext rename_rename
rename_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	eval₂_C
rename_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename X	—	eval₂_X
rename_comp_rename 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id rename	—	AlgHom.ext rename_rename
rename_eq 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename Finsupp.mapDomain Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	X_pow_eq_monomial
rename_eval₂ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename eval₂ C	—	induction_on eval₂_C algHom_C eval₂_add map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass eval₂_mul eval₂_X map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_X
rename_id 📖	mathematical	—	rename AlgHom.id MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id	—	AlgHom.ext eval₂_eta
rename_id_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	rename_id
rename_injective 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	rename_eq Finsupp.mapDomain_injective
rename_leftInverse 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	rename_rename Function.LeftInverse.comp_eq_id rename_id
rename_monomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp.mapDomain Nat.instAddCommMonoid	—	rename.eq_1 aeval_monomial monomial_eq Finsupp.prod_mapDomain_index pow_zero pow_add algebraMap_eq
rename_prod_mk_eval₂ 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename eval₂ C	—	induction_on eval₂_C algHom_C eval₂_add map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass eval₂_mul eval₂_X map_mul NonUnitalAlgSemiHomClass.toMulHomClass
rename_rename 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	rename.eq_1 eval₂_comp_left eval₂Hom_X' eval₂Hom_congr RingHom.ext eval₂Hom_C
rename_rightInverse 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	rename_leftInverse
rename_surjective 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	Function.Surjective.hasRightInverse rename_rightInverse
support_rename_of_injective 📖	mathematical	—	support DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename Finset.image Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instDecidableEq MulZeroClass.toZero Nat.instMulZeroClass Finsupp.mapDomain	—	rename_eq Finsupp.mapDomain_support_of_injective Finsupp.mapDomain_injective

---

← Back to Index