Rename

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

Statistics

Metric	Count
Definitions `killCompl`, `rename`, `renameEquiv`	3
Theorems `aeval_comp_rename`, `aeval_rename`, `coeff_killCompl`, `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_monomial`, `killCompl_monomial_eq_monomial_comapDomain_of_subset`, `killCompl_monomial_eq_zero_of_notMem_range`, `killCompl_monomial_eq_zero_of_not_subset`, `killCompl_monomial_mapDomain`, `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_eq_zero_iff_of_injective`, `rename_eval₂`, `rename_id`, `rename_id_apply`, `rename_injective`, `rename_leftInverse`, `rename_monomial`, `rename_prod_mk_eval₂`, `rename_rename`, `rename_rightInverse`, `rename_surjective`, `rename_zero`, `support_killCompl`, `support_rename_killCompl_subset`, `support_rename_of_injective`	51
Total	54

MvPolynomial

Definitions

Name	Category	Theorems
`killCompl` 📖	CompOp	12 math math: `killCompl_comp_rename`, `support_killCompl`, `killCompl_C`, `killCompl_monomial_eq_zero_of_not_subset`, `killCompl_monomial_mapDomain`, `killCompl_rename_app`, `killCompl_map`, `support_rename_killCompl_subset`, `killCompl_monomial_eq_monomial_comapDomain_of_subset`, `killCompl_monomial`, `coeff_killCompl`, `killCompl_monomial_eq_zero_of_notMem_range`
`rename` 📖	CompOp	100 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`, `rename_zero`, `bind₁_rename`, `wittStructureRat_prop`, `degrees_rename`, `Algebra.Presentation.comp_relation`, `wittStructureRat_rec`, `coeff_rename_mapDomain`, `MvPowerSeries.rename_coe`, `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`, `rename_eq_zero_iff_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`, `support_rename_killCompl_subset`, `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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `aeval` `rename`	—	`AlgHom.ext` `aeval_rename`
`aeval_rename` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `aeval` `rename`	—	`eval₂Hom_rename`
`coeff_killCompl` 📖	mathematical	—	`coeff` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `Finsupp.mapDomain` `Nat.instAddCommMonoid`	—	`induction_on'` `Function.Injective.injOn` `killCompl_monomial` `coeff_monomial` `Finsupp.mapDomain_injective` `Finsupp.mapDomain_comapDomain` `Mathlib.Tactic.Contrapose.contrapose₂` `subset_trans` `Set.instIsTransSubset` `SetLike.coe_subset_coe` `instIsConcreteLE` `Finsupp.mapDomain_support` `Finset.coe_image` `Set.preimage_range` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `coeff_add`
`coeff_rename_embDomain` 📖	mathematical	—	`coeff` `Finsupp.embDomain` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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`	`coeff` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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` `MulZeroClass.toZero` `Nat.instMulZeroClass` `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` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `constantCoeff` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.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` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`eval₂_rename`
`eval_rename_prod_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	—
`eval₂Hom_rename` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval₂Hom` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`eval₂_rename`
`eval₂_cast_comp` 📖	mathematical	—	`eval₂` `Int.instCommSemiring` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`eval₂_rename`
`eval₂_rename` 📖	mathematical	—	`eval₂` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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	—	`MvPolynomial` `DFunLike.coe` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`exists_finset_rename` `Subtype.val_injective` `Equiv.injective` `rename_rename` `Equiv.symm_apply_apply`
`exists_finset_rename` 📖	mathematical	—	`Finset` `MvPolynomial` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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	—	`Finset` `MvPolynomial` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C`	—	`algHom_C`
`killCompl_comp_rename` 📖	mathematical	—	`AlgHom.comp` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `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_monomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `Set.range` `Finsupp.comapDomain` `Function.Injective.injOn` `Set.preimage` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`Function.Injective.injOn` `killCompl_monomial_eq_monomial_comapDomain_of_subset` `killCompl_monomial_eq_zero_of_not_subset`
`killCompl_monomial_eq_monomial_comapDomain_of_subset` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.range`	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `Finsupp.comapDomain` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support`	—	`Function.Injective.injOn` `Finsupp.mapDomain_comapDomain` `killCompl_monomial_mapDomain`
`killCompl_monomial_eq_zero_of_notMem_range` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set` `Set.instMembership` `Set.range`	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`killCompl.eq_1` `aeval_monomial` `Finsupp.prod.eq_1` `mul_eq_zero_of_right` `Finset.prod_eq_zero` `zero_pow` `Finsupp.mem_support_iff`
`killCompl_monomial_eq_zero_of_not_subset` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.range`	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`Set.not_subset` `killCompl_monomial_eq_zero_of_notMem_range`
`killCompl_monomial_mapDomain` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.module` `LinearMap.instFunLike` `monomial` `Finsupp.mapDomain` `Nat.instAddCommMonoid`	—	`killCompl_rename_app`
`killCompl_rename_app` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `rename`	—	`AlgHom.congr_fun` `killCompl_comp_rename`
`map_comp_rename` 📖	mathematical	—	`RingHom.comp` `MvPolynomial` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `map` `AlgHom.toRingHom` `AddMonoidAlgebra.algebra` `Algebra.id` `rename`	—	`RingHom.ext` `map_rename`
`map_rename` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `RingHom.instFunLike` `map` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgEquiv.instFunLike` `renameEquiv` `AlgHom` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`renameEquiv_refl` 📖	mathematical	—	`renameEquiv` `Equiv.refl` `AlgEquiv.refl` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id`	—	`AlgEquiv.ext` `rename_id`
`renameEquiv_symm` 📖	mathematical	—	`AlgEquiv.symm` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `renameEquiv` `Equiv.symm`	—	—
`renameEquiv_trans` 📖	mathematical	—	`AlgEquiv.trans` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `renameEquiv` `Equiv.trans`	—	`AlgEquiv.ext` `rename_rename`
`rename_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C`	—	`eval₂_C`
`rename_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `X`	—	`eval₂_X`
`rename_comp_rename` 📖	mathematical	—	`AlgHom.comp` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `rename`	—	`AlgHom.ext` `rename_rename`
`rename_eq` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `Finsupp.mapDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`X_pow_eq_monomial`
`rename_eq_zero_iff_of_injective` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	`rename_zero` `rename_injective`
`rename_eval₂` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `eval₂` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id`	—	`AlgHom.ext` `eval₂_eta`
`rename_id_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`rename_id`
`rename_injective` 📖	mathematical	—	`MvPolynomial` `DFunLike.coe` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`rename_eq` `Finsupp.mapDomain_injective`
`rename_leftInverse` 📖	mathematical	—	`MvPolynomial` `DFunLike.coe` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`rename_rename` `Function.LeftInverse.comp_eq_id` `rename_id`
`rename_monomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Semiring.toModule` `AddMonoidAlgebra.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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `eval₂` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.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` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`rename_leftInverse`
`rename_surjective` 📖	mathematical	—	`MvPolynomial` `DFunLike.coe` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`Function.Surjective.hasRightInverse` `rename_rightInverse`
`rename_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass`	—	—
`support_killCompl` 📖	mathematical	—	`support` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `killCompl` `Finset.preimage` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.mapDomain` `Function.Injective.injOn` `Finsupp.mapDomain_injective` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.ext` `Function.Injective.injOn` `Finsupp.mapDomain_injective` `coeff_killCompl`
`support_rename_killCompl_subset` 📖	mathematical	—	`Finset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset.instHasSubset` `support` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `killCompl`	—	`support_rename_of_injective` `Function.Injective.injOn` `Finsupp.mapDomain_injective` `support_killCompl` `Finset.image_preimage` `Finset.filter_subset`
`support_rename_of_injective` 📖	mathematical	—	`support` `DFunLike.coe` `AlgHom` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `Finset.image` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instDecidableEq` `Finsupp.mapDomain`	—	`rename_eq` `Finsupp.mapDomain_support_of_injective` `Finsupp.mapDomain_injective`

---

← Back to Index