Defs

📁 Source: Mathlib/Algebra/MonoidAlgebra/Defs.lean

Statistics

Metric	Count
Definitions `AddMonoidAlgebra`, `addAddCommGroup`, `addAddCommMonoid`, `coeff`, `coeffAddEquiv`, `coeffEquiv`, `commRing`, `commSemiring`, `curryRingEquiv`, `distribSMul`, `erase`, `inhabited`, `instCoeFun`, `instDecidableEq`, `instMul`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `of`, `of'`, `ofCoeff`, `ofMagma`, `semiring`, `single`, `singleAddHom`, `singleHom`, `singleZeroRingHom`, `smulZeroClass`, `unexpander`, `unique`, `uniqueRingEquiv`, `update`, `zero`, `«term__[_]»`, `addCommGroup`, `addCommMonoid`, `coeff`, `coeffAddEquiv`, `coeffEquiv`, `commRing`, `commSemiring`, `curryRingEquiv`, `distribSMul`, `erase`, `inhabited`, `instCoeFun`, `instDecidableEq`, `instMul`, `mul'`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `of`, `ofCoeff`, `ofMagma`, `one`, `semiring`, `single`, `singleAddHom`, `singleHom`, `singleOneRingHom`, `smulZeroClass`, `unexpander`, `unique`, `uniqueRingEquiv`, `update`, `«term__[_]»`	77
Theorems `addHom_ext'`, `addHom_ext'_iff`, `coe_add`, `coeffAddEquiv_apply`, `coeffAddEquiv_symm_apply`, `coeffEquiv_apply`, `coeffEquiv_symm_apply`, `coeff_add`, `coeff_eq_zero`, `coeff_erase`, `coeff_finsuppSum`, `coeff_inj`, `coeff_injective`, `coeff_neg`, `coeff_ofCoeff`, `coeff_smul`, `coeff_sub`, `coeff_sum`, `coeff_update`, `coeff_zero`, `curryRingEquiv_single`, `curryRingEquiv_symm_single`, `erase_single`, `erase_zero`, `exists`, `ext`, `ext_iff`, `forall`, `induction_linear`, `induction_on`, `instIsCancelAdd`, `intCast_def`, `isCentralScalar`, `isLocalHom_singleZeroRingHom`, `isScalarTower`, `mul_apply`, `mul_apply_antidiagonal`, `mul_apply_left`, `mul_apply_right`, `mul_def`, `mul_single_apply`, `mul_single_apply_aux`, `mul_single_apply_of_not_exists_add`, `mul_single_zero_apply`, `natCast_def`, `neg_apply`, `nontrivial`, `of'_apply`, `of'_commute`, `of'_eq_of`, `ofCoeff_add`, `ofCoeff_coeff`, `ofCoeff_eq_zero`, `ofCoeff_erase`, `ofCoeff_finsuppSum`, `ofCoeff_inj`, `ofCoeff_injective`, `ofCoeff_neg`, `ofCoeff_smul`, `ofCoeff_sub`, `ofCoeff_sum`, `ofCoeff_update`, `ofCoeff_zero`, `ofMagma_apply`, `of_apply`, `of_injective`, `one_def`, `prod_single`, `ringHom_ext`, `ringHom_ext'`, `ringHom_ext'_iff`, `singleAddHom_apply`, `singleHom_apply`, `singleZeroRingHom_apply`, `single_add`, `single_apply`, `single_commute`, `single_commute_single`, `single_eq_zero`, `single_mul_apply`, `single_mul_apply_aux`, `single_mul_apply_of_not_exists_add`, `single_mul_single`, `single_ne_zero`, `single_neg`, `single_pow`, `single_zero`, `single_zero_comm`, `single_zero_mul_apply`, `smulCommClass`, `smul_apply`, `smul_single`, `smul_single'`, `sum_single`, `sum_single_index`, `uniqueRingEquiv_apply`, `uniqueRingEquiv_symm_apply`, `addHom_ext'`, `addHom_ext'_iff`, `coe_add`, `coeffAddEquiv_apply`, `coeffAddEquiv_symm_apply`, `coeffEquiv_apply`, `coeffEquiv_symm_apply`, `coeff_add`, `coeff_eq_zero`, `coeff_erase`, `coeff_finsuppSum`, `coeff_inj`, `coeff_injective`, `coeff_neg`, `coeff_ofCoeff`, `coeff_smul`, `coeff_sub`, `coeff_sum`, `coeff_update`, `coeff_zero`, `curryRingEquiv_single`, `curryRingEquiv_symm_single`, `erase_single`, `erase_zero`, `exists`, `ext`, `ext_iff`, `forall`, `induction_linear`, `induction_on`, `instIsCancelAdd`, `intCast_def`, `isCentralScalar`, `isLocalHom_singleOneRingHom`, `isScalarTower`, `mul_apply`, `mul_apply_antidiagonal`, `mul_apply_left`, `mul_apply_right`, `mul_def`, `mul_single_apply`, `mul_single_apply_aux`, `mul_single_apply_of_not_exists_mul`, `mul_single_one_apply`, `natCast_def`, `neg_apply`, `nontrivial`, `ofCoeff_add`, `ofCoeff_coeff`, `ofCoeff_eq_zero`, `ofCoeff_erase`, `ofCoeff_finsuppSum`, `ofCoeff_inj`, `ofCoeff_injective`, `ofCoeff_neg`, `ofCoeff_smul`, `ofCoeff_sub`, `ofCoeff_sum`, `ofCoeff_update`, `ofCoeff_zero`, `ofMagma_apply`, `of_apply`, `of_commute`, `of_injective`, `one_def`, `prod_single`, `ringHom_ext`, `ringHom_ext'`, `ringHom_ext'_iff`, `singleAddHom_apply`, `singleHom_apply`, `singleOneRingHom_apply`, `single_add`, `single_apply`, `single_commute`, `single_commute_single`, `single_eq_zero`, `single_mul_apply`, `single_mul_apply_aux`, `single_mul_apply_of_not_exists_mul`, `single_mul_single`, `single_ne_zero`, `single_neg`, `single_one_comm`, `single_one_mul_apply`, `single_pow`, `single_zero`, `smulCommClass`, `smul_apply`, `smul_single`, `smul_single'`, `sum_single`, `sum_single_index`, `uniqueRingEquiv_apply`, `uniqueRingEquiv_symm_apply`	192
Total	269

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`addAddCommGroup` 📖	CompOp	46 math math: `MvPolynomial.coeff_neg`, `MvPolynomial.degrees_neg`, `DirectSum.toAddMonoidAlgebra_sub`, `ofCoeff_neg`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `coeff_sub`, `neg_apply`, `MvPolynomial.eval₂_neg`, `ofCoeff_sub`, `MonomialOrder.degree_neg`, `MvPolynomial.quotient_map_C_eq_zero`, `WittVector.mul_polyOfInterest_aux4`, `MvPolynomial.eval_neg`, `supDegree_neg`, `map_sub`, `MvPolynomial.vars_neg`, `MvPolynomial.totalDegree_neg`, `MvPolynomial.support_neg`, `MonomialOrder.sPolynomial_antisymm`, `MvPolynomial.mul_esymm_eq_sum`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul`, `Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul`, `Polynomial.ofFinsupp_neg`, `MonomialOrder.leadingCoeff_neg`, `MvPolynomial.C_neg`, `Polynomial.toFinsupp_neg`, `toDirectSum_sub`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul`, `WittVector.wittNeg_zero`, `supDegree_sub_le`, `MvPolynomial.psum_eq_mul_esymm_sub_sum`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `toDirectSum_neg`, `map_neg`, `single_neg`, `StandardEtalePresentation.toPresentation_relation`, `WittVector.mul_polyOfInterest_aux3`, `MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix`, `MvPolynomial.IsHomogeneous.neg`, `DirectSum.toAddMonoidAlgebra_neg`, `MvPolynomial.degreeOf_neg`, `coeff_neg`, `MvPolynomial.IsSymmetric.neg`, `Polynomial.homogenize_neg`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val`
`addAddCommMonoid` 📖	CompOp	527 math math: `MvPolynomial.pUnitAlgEquiv_symm_monomial`, `MvPolynomial.aeval_sum`, `MvPolynomial.dvd_monomial_one_iff_exists`, `supDegree_sum_lt`, `supportedEquivFinsupp_apply_apply`, `MvPowerSeries.WithPiTopology.tendsto_trunc_atTop`, `MvPolynomial.support_sum`, `MonomialOrder.sPolynomial_leadingTerm_mul'`, `Algebra.PreSubmersivePresentation.jacobiMatrix_naive`, `MvPolynomial.vars_sum_of_disjoint`, `MvPolynomial.totalDegree_monomial`, `MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum`, `MvPowerSeries.eq_iff_frequently_trunc'_eq`, `MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_same`, `MvPowerSeries.truncFinset_one`, `MvPowerSeries.trunc'_trunc'`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_apply`, `MvPolynomial.rTensor_apply_tmul_apply`, `MvPolynomial.degrees_monomial`, `liftNC_mul`, `MvPolynomial.rTensorAlgEquiv_apply`, `MvPolynomial.one_def`, `Algebra.Generators.H1Cotangent.δAux_mul`, `of'_mem_span`, `MvPolynomial.scalarRTensor_apply_monomial_tmul`, `MvPolynomial.homogeneousComponent_eq_zero'`, `LaurentPolynomial.comul_T`, `MvPolynomial.universalFactorizationMap_comp_map`, `MonomialOrder.degree_monomial`, `comapDomain_add`, `MvPolynomial.IsWeightedHomogeneous.pderiv`, `MvPolynomial.X_pow_eq_monomial`, `le_infDegree_add`, `LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply`, `comul_single`, `isScalarTower_self`, `MvPolynomial.leibniz_iff_X`, `Polynomial.homogenize_smul`, `MvPolynomial.divMonomial_add_modMonomial`, `MvPowerSeries.trunc'_expand_trunc'`, `MvPolynomial.eval₂Hom_monomial`, `MvPolynomial.homogeneousComponent_of_mem`, `MvPolynomial.homogeneousComponent_mem`, `MvPolynomial.support_monomial`, `MvPolynomial.monomial_finsupp_sum_index`, `MvPolynomial.weightedHomogeneousSubmodule_mul`, `MvPolynomial.mul_def`, `MvPolynomial.scalarRTensor_apply_X_tmul_apply`, `MvPowerSeries.ext_trunc'`, `MvPolynomial.smul_monomial`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff`, `MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same`, `ofCoeff_eq_zero`, `supportedEquivFinsupp_apply_support_val`, `MvPolynomial.pderiv_one`, `MvPolynomial.pderiv_mul`, `MvPolynomial.degreeOf_sum_le`, `supDegree_add_le`, `PolynomialLaw.exists_lift'`, `divOfHom_apply_apply`, `MvPolynomial.monomial_zero`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `MvPowerSeries.trunc_C`, `Polynomial.eval₂_ofFinsupp`, `Algebra.Generators.cotangentSpaceBasis_repr_one_tmul`, `MvPolynomial.pderiv_rename`, `MvPolynomial.monomial_eq_monomial_iff`, `MvPolynomial.eval₂_mul_monomial`, `MvPolynomial.weightedHomogeneousComponent_zero`, `coeff_add`, `MvPolynomial.homogeneousComponent_C_mul`, `MvPolynomial.instFree`, `MvPolynomial.weightedDecomposition.decompose'_apply`, `MvPolynomial.expand_monomial`, `MvPolynomial.monomial_mul_mem_coeffsIn`, `singleZeroRingHom_apply`, `MvPowerSeries.coeff_truncFinset_of_mem`, `Algebra.Generators.H1Cotangent.δAux_C`, `MvPolynomial.eval₂_sum`, `MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero`, `instIsTorsionFree`, `counit_single`, `smulCommClass`, `MvPolynomial.X_mul_pderiv_monomial`, `coeff_sum`, `MvPolynomial.weightedHomogeneousComponent_eq_zero'`, `MvPowerSeries.trunc'_trunc'_pow`, `moduleFinite`, `MvPolynomial.homogeneousComponent_isHomogeneous`, `MvPolynomial.sum_homogeneousComponent`, `MvPolynomial.degreesLE_nsmul`, `MvPolynomial.coe_monomial`, `MvPolynomial.C_apply`, `LieAlgebra.LoopAlgebra.toFinsupp_symm_single`, `decomposeAux_coe`, `lsingle_apply`, `MvPolynomial.single_eq_monomial`, `gradeBy.isInternal`, `MvPowerSeries.trunc_one`, `MvPolynomial.mul_X_mem_coeffsIn`, `single_add`, `smul_single`, `MonomialOrder.leadingTerm_monomial`, `MvPolynomial.X_mul_mem_coeffsIn`, `xInTermsOfW_eq`, `MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul`, `MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring`, `MvPolynomial.degreesLE_add`, `MonomialOrder.span_leadingTerm_eq_span_monomial`, `MonomialOrder.span_leadingTerm_eq_span_monomial₀`, `MvPolynomial.scalarRTensor_apply_tmul`, `tensorEquiv.invFun_tmul`, `MvPolynomial.C_mul_X_eq_monomial`, `erase_zero`, `MvPolynomial.bind₂_monomial`, `smul_apply`, `MvPolynomial.monomialOneHom_apply`, `smulCommClass_symm_self`, `le_inf_support_add`, `Algebra.SubmersivePresentation.jacobianRelations_spec`, `MvPolynomial.pderiv_sumToIter`, `MvPolynomial.coeff_homogeneousComponent`, `MvPolynomial.monomial_left_inj`, `MvPolynomial.X_dvd_monomial`, `Algebra.PreSubmersivePresentation.jacobiMatrix_apply`, `isScalarTower`, `MvPolynomial.C_mul_monomial`, `Algebra.Generators.H1Cotangent.δAux_monomial`, `MvPolynomial.vars_monomial`, `MvPolynomial.pow_idealOfVars_eq_span`, `MvPolynomial.IsWeightedHomogeneous.sum`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `MvPolynomial.bind₂_monomial_one`, `supDegree_zero`, `MvPolynomial.rTensor_apply_X_tmul`, `Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation`, `MvPolynomial.pderiv_X`, `MvPolynomial.restrictSupport_univ`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `mul_def`, `PolynomialLaw.exists_lift`, `MvPolynomial.coeff_sum_X_pow_of_fintype`, `MvPolynomial.coeff_smul`, `MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval`, `MvPolynomial.finitePresentation_universalFactorizationMap`, `MvPolynomial.map_restrict_dom_evalₗ`, `MvPolynomial.tensorEquivSum_one_tmul_C`, `MvPolynomial.rTensor_apply_tmul`, `MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne`, `MvPolynomial.coeff_monomial_mul`, `MvPolynomial.dvd_monomial_iff_exists`, `comapDomainAddMonoidHom_apply`, `MonomialOrder.degree_sum_le`, `MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum`, `MvPolynomial.mkDerivationₗ_monomial`, `MvPolynomial.killCompl_monomial_eq_zero_of_not_subset`, `MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv`, `toDirectSum_zero`, `MvPolynomial.sum_weightedHomogeneousComponent`, `MvPowerSeries.truncFinset_C`, `MvPolynomial.pderiv_def`, `MvPolynomial.modMonomial_add_divMonomial`, `MonomialOrder.span_leadingTerm_eq_span_monomial'`, `toDirectSum_add`, `coe_add`, `MvPolynomial.decompose'_apply`, `MvPowerSeries.truncFinset_map`, `leadingCoeff_zero`, `MvPolynomial.monomial_one_mul_cancel_left_iff`, `MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul`, `MvPolynomial.coe_basisMonomials`, `xInTermsOfW_aux`, `MvPolynomial.monomial_mem_pow_idealOfVars_iff`, `MvPolynomial.irreducible_sumSMulX`, `Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp`, `MvPowerSeries.truncFinset_monomial_eq_zero`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `MvPolynomial.finite_universalFactorizationMap`, `MvPolynomial.rTensorAlgHom_toLinearMap`, `wittStructureRat_rec`, `MvPolynomial.homogeneousSubmodule_zero`, `MvPolynomial.coeff_sumSMulX`, `MvPowerSeries.trunc'_expand`, `MvPolynomial.universalFactorizationMapPresentation_map`, `MvPolynomial.restrictSupport_mono`, `MvPolynomial.algebraTensorAlgEquiv_symm_X`, `MvPolynomial.mem_restrictDegree`, `MonomialOrder.monic_monomial`, `MvPolynomial.indicator_mem_restrictDegree`, `MvPolynomial.coeffsIn_mul`, `MonomialOrder.sPolynomial_def`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `MvPolynomial.restrictSupport_zero`, `MvPolynomial.killCompl_monomial_mapDomain`, `MvPolynomial.as_sum`, `MonomialOrder.leadingCoeff_monomial`, `MvPolynomial.monomial_add_single`, `MvPolynomial.le_coeffsIn_pow`, `MvPowerSeries.trunc_map`, `MonomialOrder.monic_monomial_one`, `MvPolynomial.monomial_eq_zero`, `coeffLinearEquiv_apply`, `MvPolynomial.eval_monomial`, `MvPolynomial.coeff_monomial_mul'`, `MvPolynomial.monomial_mem_coeffsIn`, `MvPowerSeries.coeff_trunc'`, `wittStructureRat_rec_aux`, `MonomialOrder.sPolynomial_decomposition`, `MvPolynomial.constantCoeff_smul`, `LaurentPolynomial.leval_apply`, `faithfulSMul`, `MvPowerSeries.coeff_trunc`, `MvPolynomial.mkDerivation_monomial`, `MvPolynomial.degrees_sum_le`, `MvPolynomial.rename_monomial`, `MvPolynomial.mul_esymm_eq_sum`, `MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite`, `MvPolynomial.mem_restrictSupport_iff`, `MvPolynomial.degreesLE_zero`, `GradesBy.decompose_single`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `Algebra.PreSubmersivePresentation.aevalDifferential_single`, `MvPolynomial.isWeightedHomogeneous_monomial`, `singleAddHom_apply`, `coe_liftNCAlgHom`, `MvPolynomial.monomial_zero'`, `Polynomial.homogenize_finsetSum`, `Polynomial.ofFinsupp_smul`, `MvPolynomial.weightedHomogeneousComponent_directSum`, `supported_eq_span_single`, `mem_grade_iff'`, `MvPowerSeries.truncFinset_monomial`, `coeff_smul`, `MvPolynomial.homogeneousComponent_apply`, `MvPolynomial.divMonomial_mul_monomial`, `MvPolynomial.weightedHomogeneousComponent_finsupp`, `MvPolynomial.coeff_linearCombination_X_pow`, `comapDomain_zero`, `MvPolynomial.linearIndependent_X`, `MvPolynomial.prod_X_pow_eq_monomial`, `MvPolynomial.constantCoeff_monomial`, `MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap`, `MvPolynomial.coeff_rTensorAlgHom_tmul`, `MvPolynomial.mem_weightedHomogeneousSubmodule`, `MvPolynomial.divMonomial_monomial`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `WittVector.frobeniusPolyAux_eq`, `DirectSum.toAddMonoidAlgebra_zero`, `LieAlgebra.LoopAlgebra.toFinsupp_single_tmul`, `ofCoeff_zero`, `MvPolynomial.mem_coeffsIn`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne`, `MvPolynomial.isHomogeneous_monomial`, `supported_eq_map`, `MvPolynomial.pderiv_C_mul`, `Module.Basis.symmetricAlgebra_repr_apply`, `single_mem_grade`, `Polynomial.toFinsuppIsoLinear_apply`, `MvPolynomial.decomposition.decompose'_apply`, `MvPolynomial.restrictSupport_nsmul`, `coeffAddEquiv_symm_apply`, `MvPolynomial.psum_one`, `MvPolynomial.mem_degreesLE`, `MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous`, `LaurentPolynomial.comul_C`, `MvPolynomial.map_monomial`, `liftNC_smul`, `MvPolynomial.monomial_mem_restrictSupport`, `MvPolynomial.homogeneousComponent_eq_zero`, `liftNC_single`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs`, `MonomialOrder.sPolynomial_monomial_mul`, `MvPolynomial.mem_homogeneousSubmodule`, `ofCoeff_add`, `MvPolynomial.homogeneousComponent_zero`, `MvPolynomial.ker_eval₂Hom_universalFactorizationMap`, `MvPolynomial.monomial_left_injective`, `MvPolynomial.monomial_sum_index`, `smul_single'`, `MvPolynomial.monic_monomial_eq`, `supDegree_leadingCoeff_sum_eq`, `map_add`, `MvPolynomial.pderiv_monomial_single`, `tensorEquiv_tmul`, `gradeBy.gradedMonoid`, `MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite`, `MvPolynomial.DirectSum.coeLinearMap_eq_finsum`, `WittVector.mul_polyOfInterest_aux1`, `MvPolynomial.support_monomial_subset`, `MvPolynomial.monomial_mul`, `coeff_eq_zero`, `MvPowerSeries.totalDegree_trunc'`, `MvPolynomial.rTensor_symm_apply_single`, `MvPolynomial.pderiv_X_of_ne`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `MvPolynomial.pderiv_monomial`, `Algebra.Generators.toComp_toAlgHom_monomial`, `erase_single`, `MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree`, `tensorEquiv_symm_single`, `MvPolynomial.finrank_eq_zero`, `MvPolynomial.dvd_monomial_mul_iff_exists`, `mem_grade_iff`, `Algebra.Generators.H1Cotangent.δAux_X`, `MonomialOrder.div_set`, `grade.decompose_single`, `single_eq_zero`, `MvPolynomial.mem_restrictDegree_iff_sup`, `MvPolynomial.hsymm_one`, `MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem`, `LieAlgebra.LoopAlgebra.residuePairing_apply_apply`, `MvPolynomial.rTensor_apply_monomial_tmul`, `Algebra.Generators.repr_CotangentSpaceMap`, `MvPolynomial.pderiv_pow`, `coeffLinearEquiv_symm_apply`, `lhom_ext'_iff`, `MvPolynomial.mkDerivationₗ_C`, `MvPolynomial.totalDegree_finsetSum_le`, `single_zero`, `MvPolynomial.support_smul_eq`, `MvPolynomial.tensorEquivSum_X_tmul_X`, `MvPolynomial.coeff_rTensorAlgHom_monomial_tmul`, `MvPolynomial.support_sum_monomial_coeff`, `MvPolynomial.mem_coeffsIn_iff_coeffs_subset`, `MvPolynomial.algebraTensorAlgEquiv_symm_map`, `MvPolynomial.weightedDecomposition.decompose'_eq`, `MvPolynomial.tensorEquivSum_C_tmul_one`, `coeff_finsuppSum`, `Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one`, `Polynomial.toFinsupp_sum`, `supported_mono`, `MvPolynomial.coeffsIn_eq_span_monomial`, `Algebra.Generators.ofComp_toAlgHom_monomial_sumElim`, `Algebra.Presentation.algebraTensorAlgEquiv_symm_relation`, `MvPolynomial.coeffsIn_pow`, `MvPolynomial.monomial_eq`, `LaurentPolynomial.counit_C_mul_T`, `basis_apply`, `MvPolynomial.pderiv_map`, `MvPolynomial.esymm_eq_sum_monomial`, `DirectSum.toAddMonoidAlgebra_add`, `grade.isInternal`, `MvPolynomial.HomogeneousSubmodule.gradedMonoid`, `MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc'`, `MvPolynomial.instFiniteOfIsEmpty`, `MvPolynomial.weightedHomogeneousComponent_eq_zero`, `MvPolynomial.restrictSupport_add`, `MvPolynomial.totalDegree_monomial_le`, `MvPowerSeries.totalDegree_truncFinset`, `MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop`, `Polynomial.toFinsupp_smul`, `mapDomain_zero`, `MvPolynomial.pderiv_inr_universalFactorizationMap_X`, `coeffAddEquiv_apply`, `MvPolynomial.weightedHomogeneousComponent_C_mul`, `liftNC_one`, `MvPolynomial.mul_monomial_mem_coeffsIn`, `MvPolynomial.IsHomogeneous.sum`, `scalarTensorEquiv_symm_single`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `MonomialOrder.sPolynomial_monomial_mul'`, `supportedEquivFinsupp_symm_apply_coe_apply`, `MvPolynomial.pderiv_eq_zero_of_notMem_vars`, `sup_support_add_le`, `MvPolynomial.msymm_one`, `MvPolynomial.C_mul_X_pow_eq_monomial`, `MvPolynomial.weightedHomogeneousComponent_mem`, `MvPolynomial.psum_eq_mul_esymm_sub_sum`, `Algebra.Generators.cotangentRestrict_mk`, `MvPolynomial.optionEquivLeft_monomial`, `ofCoeff_sum`, `Algebra.Generators.H1Cotangent.δ_eq_δAux`, `instIsCocomm`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `MvPowerSeries.coeff_truncFinset_eq_zero`, `MvPolynomial.algebraTensorAlgEquiv_tmul`, `MvPolynomial.homogeneousSubmodule_one_eq_span_X`, `instFree`, `LaurentPolynomial.instIsCocomm`, `LaurentPolynomial.counit_T`, `MvPolynomial.totalDegree_finset_sum`, `LaurentPolynomial.counit_C`, `MvPolynomial.divMonomial_monomial_mul`, `MvPolynomial.sum_monomial_eq`, `MvPolynomial.degrees_monomial_eq`, `MvPolynomial.pUnitAlgEquiv_monomial`, `MvPolynomial.coeff_monomial`, `MvPolynomial.coeff_mul_monomial`, `MvPolynomial.mem_ideal_span_monomial_image_iff_dvd`, `IsRegular.monomial`, `MvPolynomial.monomial_pow`, `MvPolynomial.eval_sum`, `MvPolynomial.eval₂_monomial`, `LaurentPolynomial.comul_C_mul_T`, `MvPolynomial.homogeneousSubmodule_one_pow`, `MvPolynomial.prod_X_pow`, `MvPolynomial.universalFactorizationMapPresentation_algebra_smul`, `MvPolynomial.IsHomogeneous.sum_X_mul_pderiv`, `MvPolynomial.aeval_sumElim_pderiv_inl`, `MvPolynomial.monomial_one_dvd_monomial_one`, `MvPolynomial.mul_monomial_modMonomial`, `MvPolynomial.tensorEquivSum_one_tmul_X`, `MvPolynomial.one_coeffsIn`, `MvPolynomial.mkDerivationₗ_X`, `mem_supported'`, `MvPolynomial.universalFactorizationMap_freeMonic`, `Algebra.Generators.Hom.toAlgHom_monomial`, `MvPolynomial.universalFactorizationMapPresentation_val`, `mem_span_support'`, `MvPolynomial.universalFactorizationMapPresentation_σ'`, `LaurentPolynomial.smul_eq_C_mul`, `decomposeAux_single`, `ofCoeff_finsuppSum`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `MvPolynomial.coeff_linearCombination_X_pow_of_fintype`, `MvPolynomial.monomial_sum_one`, `MvPowerSeries.truncFinset_truncFinset`, `MvPolynomial.totalDegree_smul_le`, `MvPowerSeries.support_truncFinset_subset`, `MvPowerSeries.coeff_truncFinset`, `MonomialOrder.div`, `MvPolynomial.scalarRTensor_symm_apply_single`, `addHom_ext'_iff`, `addMonoidAlgebraAddEquivDirectSum_symm_apply`, `MvPolynomial.weightedHomogeneousComponent_of_mem`, `MvPolynomial.irreducible_sumSMulXSMulY`, `MvPolynomial.mem_ideal_span_monomial_image`, `decomposeAux_eq_decompose`, `MvPolynomial.coeff_weightedHomogeneousComponent`, `MvPolynomial.rTensor_apply`, `mapDomain_add`, `MvPolynomial.C_mem_coeffsIn`, `MvPolynomial.disjoint_support_monomial`, `MvPolynomial.aeval_monomial`, `lift_def`, `instIsCancelAdd`, `ofCoeff_smul`, `coeff_zero`, `addMonoidAlgebraAddEquivDirectSum_apply`, `MonomialOrder.degree_monomial_le`, `MvPolynomial.esymm_eq_sum_subtype`, `MvPolynomial.coeff_mul_monomial'`, `MvPolynomial.pderiv_X_self`, `MvPolynomial.pderiv_C`, `MvPowerSeries.trunc'_one`, `MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix`, `scalarTensorEquiv_tmul`, `MvRatFunc.rank_eq_max_lift`, `MvPolynomial.homogeneousSubmodule_mul`, `Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `MvPowerSeries.trunc_C_mul`, `MvPolynomial.lcoeff_apply`, `MvPolynomial.algebraTensorAlgEquiv_symm_monomial`, `MvPolynomial.restrictSupport_eq_span`, `MvPolynomial.rank_eq`, `MvPolynomial.esymm_one`, `distribMulActionHom_ext'_iff`, `Polynomial.ofFinsupp_sum`, `MvPolynomial.finrank_eq_one`, `sum_single`, `MvPowerSeries.trunc'_map`, `MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset`, `MvPolynomial.tensorEquivSum_X_tmul_one`, `map_sum`, `MvPolynomial.killCompl_monomial`, `single_mem_gradeBy`, `MonomialOrder.sPolynomial_decomposition'`, `MvPolynomial.scalarRTensor_apply_tmul_apply`, `grade.gradedMonoid`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `MvPolynomial.coeffsIn_le`, `MonomialOrder.C_mul_leadingCoeff_monomial_degree`, `Algebra.Generators.comp_σ`, `MvPolynomial.support_smul`, `MvPowerSeries.truncFinset_apply`, `MvPolynomial.tensorEquivSum_C_tmul_C`, `MvPolynomial.finsum_weightedHomogeneousComponent`, `isCentralScalar`, `LaurentPolynomial.comul_C_mul_T_self`, `LaurentPolynomial.instIsScalarTowerPolynomial`, `MvPolynomial.linearMap_ext_iff`, `MvPolynomial.monomial_single_add`, `wittPolynomial_eq_sum_C_mul_X_pow`, `MvPolynomial.monomial_one_mul_cancel_right_iff`, `Polynomial.homogenizeLM_apply`, `MvPolynomial.degreeOf_monomial_eq`, `map_zero`, `smulCommClass_self`, `rank_mvPolynomial_mvPolynomial`, `MvPolynomial.vars_sum_subset`, `mem_gradeBy_iff`, `mapDomain_sum`, `MvPolynomial.weightedHomogeneousComponent_apply`, `mem_span_support`, `MvPolynomial.rank_eq_lift`, `MvPolynomial.IsHomogeneous.pderiv`, `MvPolynomial.mem_restrictTotalDegree`, `MvPolynomial.restrictTotalDegree_le_restrictDegree`, `Algebra.SubmersivePresentation.basisDeriv_apply`, `MvPolynomial.bind₁_monomial`, `MvPolynomial.induction_on_monomial`, `MvPolynomial.coe_coeffsIn`, `MvPolynomial.vars_monomial_single`, `MvPolynomial.evalₗ_apply`, `MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range`, `MvPolynomial.monomial_modMonomial`, `MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid`, `MonomialOrder.sPolynomial_mul_monomial`, `MvPowerSeries.trunc'_C`, `MvPolynomial.decomposition.decompose'_eq`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `MonomialOrder.sPolynomial_leadingTerm_mul`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap`, `MvPolynomial.coeff_sum`, `MvPowerSeries.trunc'_C_mul`, `Polynomial.homogenize_monomial`, `MvPowerSeries.truncFinset_truncFinset_pow`, `mem_supported`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'`, `supDegree_sum_le`, `MvPolynomial.monomial_dvd_monomial`, `MvPolynomial.monomial_mul_modMonomial`, `MvPolynomial.pderiv_inl_universalFactorizationMap_X`, `MvPolynomial.rTensorAlgHom_apply_eq`
`coeff` 📖	CompOp	23 math math: `supportedEquivFinsupp_apply_apply`, `coeff_comapDomain`, `supportedEquivFinsupp_apply_support_val`, `ofCoeff_coeff`, `coeff_add`, `coeff_sub`, `coeff_sum`, `coeffLinearEquiv_apply`, `coeff_smul`, `coeff_eq_zero`, `coeff_finsuppSum`, `coeffAddEquiv_apply`, `coeff_injective`, `coeff_ofCoeff`, `mem_supported'`, `coeff_inj`, `coeff_zero`, `coeff_neg`, `coeffEquiv_apply`, `coeff_erase`, `coeff_update`, `coeff_map`, `mem_supported`
`coeffAddEquiv` 📖	CompOp	2 math math: `coeffAddEquiv_symm_apply`, `coeffAddEquiv_apply`
`coeffEquiv` 📖	CompOp	2 math math: `coeffEquiv_symm_apply`, `coeffEquiv_apply`
`commRing` 📖	CompOp	132 math math: `AlgebraicGeometry.AffineSpace.map_Spec_map`, `KaehlerDifferential.mvPolynomialBasis_apply`, `Algebra.PreSubmersivePresentation.jacobiMatrix_naive`, `MvPolynomial.isJacobsonRing`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc`, `CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd`, `AlgebraicIndependent.of_aeval`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv`, `Algebra.Presentation.naive_toGenerators`, `MvPolynomial.universalFactorizationMap_comp_map`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_map`, `Algebra.Generators.cotangentSpaceBasis_apply`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop`, `LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply`, `KaehlerDifferential.mvPolynomialBasis_repr_D_X`, `StandardEtalePresentation.toPresentation_algebra_smul`, `Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp`, `Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_relation`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_σ'`, `Algebra.Presentation.quotientEquiv_symm`, `Algebra.Generators.naive_val`, `instIsIntegralMvPolynomial`, `Algebra.Generators.compLocalizationAwayAlgHom_X_inl`, `Algebra.Presentation.naive_relation`, `StandardEtalePair.equivMvPolynomialQuotient_symm_apply`, `Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial`, `MvPolynomial.transcendental_supported_X_iff`, `MvPolynomial.algebraicIndependent_polynomial_aeval_X`, `Algebra.SubmersivePresentation.jacobianRelations_spec`, `TensorProduct.toIntegralClosure_mvPolynomial_bijective`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply`, `MvPolynomial.quotient_map_C_eq_zero`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `AlgebraicIndependent.lift_reprField`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `IsLocalization.Away.mvPolynomialQuotientEquiv_apply`, `Algebra.Presentation.naive_relation_apply`, `MvPolynomial.finitePresentation_universalFactorizationMap`, `Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord`, `Algebra.PreSubmersivePresentation.naive_toPresentation`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `MvPolynomial.finite_universalFactorizationMap`, `MvPolynomial.universalFactorizationMapPresentation_map`, `CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly`, `MvPolynomial.mk_eq_eval₂`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `exists_integral_inj_algHom_of_quotient`, `exists_finite_inj_algHom_of_fg`, `Algebra.FinitePresentation.iff`, `MvPolynomial.mkₐ_eq_aeval`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul`, `MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul`, `AlgebraicGeometry.AffineSpace.map_SpecMap`, `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc`, `Algebra.Generators.toKaehler_tmul_D`, `MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing`, `AlgebraicIndependent.liftAlgHom_comp_reprField`, `RingHom.IsStandardSmooth.exists_etale_mvPolynomial`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply`, `MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse`, `MvPolynomial.quotient_mk_comp_C_injective`, `AlgebraicClosure.Monics.map_eq_prod`, `StandardEtalePresentation.toPresentation_σ'`, `MvPolynomial.isIntegral_iff_isIntegral_coeff`, `Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop`, `Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one`, `MvPolynomial.algebraicIndependent_X`, `AlgebraicIndependent.aevalEquivField_apply_coe`, `IsTranscendenceBasis.mvPolynomial`, `Algebra.Generators.naive_σ`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst`, `AlgebraicGeometry.AffineSpace.over_over`, `IsTranscendenceBasis.mvPolynomial'`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp`, `StandardEtalePresentation.toPresentation_val`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `Algebra.mvPolynomial`, `MvPolynomial.universalFactorizationMapPresentation_algebra_smul`, `Algebra.Generators.Hom.toAlgHom_monomial`, `MvPolynomial.universalFactorizationMapPresentation_val`, `MvPolynomial.universalFactorizationMapPresentation_σ'`, `KaehlerDifferential.mvPolynomialBasis_repr_symm_single`, `AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `Algebra.Presentation.quotientEquiv_mk`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over`, `MvPolynomial.isJacobsonRing_MvPolynomial_fin`, `MvPolynomial.transcendental_supported_polynomial_aeval_X_iff`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over`, `StandardEtalePresentation.toPresentation_relation`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_val`, `MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse`, `MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul`, `MvRatFunc.rank_eq_max_lift`, `LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe`, `RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`, `MvPolynomial.trdeg_of_isDomain`, `MvPolynomial.transcendental_supported_X`, `Algebra.Presentation.instFinitePresentationQuotientOfFinite`, `exists_integral_inj_algHom_of_fg`, `Algebra.Generators.ker_naive`, `instFreeMvPolynomialKaehlerDifferential`, `Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`, `Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det`, `Algebra.Presentation.mem_ker_naive`, `instIsPushoutFractionRingMvPolynomial_1`, `Algebra.Generators.toExtension_commRing`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `MvPolynomial.transcendental_supported_polynomial_aeval_X`, `instIsPushoutFractionRingMvPolynomial`, `Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val`
`commSemiring` 📖	CompOp	246 math math: `Algebra.PreSubmersivePresentation.jacobiMatrix_naive`, `MvPolynomial.radical_le_vanishingIdeal_zeroLocus`, `MvPolynomial.aeval_X_left`, `LaurentPolynomial.mk'_one_X_pow`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_apply`, `LaurentPolynomial.mk'_mul_T`, `Algebra.Generators.H1Cotangent.δAux_mul`, `MvPolynomial.isOpenMap_comap_C`, `MvPolynomial.universalFactorizationMap_comp_map`, `MvPolynomial.derivation_eq_of_forall_mem_vars`, `Algebra.Generators.cotangentSpaceBasis_apply`, `MvPolynomial.IsWeightedHomogeneous.pderiv`, `MvPolynomial.iterToSum_sumToIter`, `MvPolynomial.aeval_X_left_apply`, `MvPolynomial.monomial_finsupp_sum_index`, `StandardEtalePresentation.toPresentation_algebra_smul`, `MvPolynomial.image_comap_C_basicOpen`, `LaurentPolynomial.mk'_one_X`, `chevalley_mvPolynomial_mvPolynomial`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff`, `MvPolynomial.optionEquivLeft_apply`, `MvPolynomial.instIsScalarTower`, `MvPolynomial.prime_rename_iff`, `MvPolynomial.eval₂_prod`, `MvPolynomial.iterToSum_C_X`, `MvPolynomial.map_eval₂`, `Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap`, `MvPolynomial.pderiv_one`, `MvPolynomial.mkDerivation_X`, `MvPolynomial.pderiv_mul`, `Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp`, `MvPolynomial.aeval_ite_mem_eq_self`, `MvPolynomial.eval₂Hom_C_id_eq_join₁`, `Algebra.Generators.algebraMap_surjective`, `MvPolynomial.pow_idealOfVars`, `MvPolynomial.join₂_comp_map`, `PolynomialLaw.toFun_eq_rTensor_φ_toFun'`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `MvPolynomial.eval_eval₂`, `MvPolynomial.eval₂Hom_C_eq_bind₁`, `MvPolynomial.mem_pow_idealOfVars_iff`, `MvPolynomial.X_prime`, `Algebra.Generators.cotangentSpaceBasis_repr_one_tmul`, `MvPolynomial.pderiv_rename`, `algebraMap_def`, `Algebra.Presentation.quotientEquiv_symm`, `MvPolynomial.sumAlgEquiv_comp_rename_inr`, `MvPolynomial.X_mul_pderiv_monomial`, `MonomialOrder.leadingCoeff_prod_of_regular`, `Algebra.Generators.algebraMap_apply`, `MvPolynomial.derivation_eq_zero_of_forall_mem_vars`, `Algebra.Generators.compLocalizationAwayAlgHom_X_inl`, `ChevalleyThm.chevalley_mvPolynomialC`, `mvPolynomial_aeval_of_surjective_of_closure`, `Algebra.Generators.algebraMap_eq`, `Algebra.SubmersivePresentation.ofSubsingleton_relation`, `Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial`, `MvPolynomial.transcendental_supported_X_iff`, `MvPolynomial.vanishingIdeal_pointToPoint`, `MvPolynomial.optionEquivRight_symm_apply`, `MvPolynomial.eval_prod`, `Algebra.Presentation.comp_aeval_relation_inl`, `MvPolynomial.totalDegree_finset_prod`, `MvPolynomial.pderiv_sumToIter`, `sup_support_multiset_prod_le`, `MonomialOrder.coeff_prod_sum_degree`, `Algebra.PreSubmersivePresentation.jacobiMatrix_apply`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply`, `MvPolynomial.iterToSum_X`, `MvPolynomial.pow_idealOfVars_eq_span`, `MvPolynomial.commAlgEquiv_C`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `MvPolynomial.commAlgEquiv_X`, `Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation`, `MvPolynomial.pderiv_X`, `MvPolynomial.uniqueFactorizationMonoid`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `prod_single`, `MvPolynomial.rename_eval₂`, `LaurentPolynomial.mk'_eq`, `MvPolynomial.finitePresentation_universalFactorizationMap`, `MvPolynomial.totalDegree_multiset_prod`, `Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom`, `MvPolynomial.bind₂_id`, `MvPolynomial.sumAlgEquiv_comp_rename_inl`, `MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv`, `MvPolynomial.pderiv_def`, `MvPolynomial.mem_pow_idealOfVars_iff'`, `MvPolynomial.monomial_mem_pow_idealOfVars_iff`, `Algebra.Generators.instIsScalarTowerRing`, `MvPolynomial.finite_universalFactorizationMap`, `MvPolynomial.isRegular_prod_X`, `MvPolynomial.universalFactorizationMapPresentation_map`, `MvPolynomial.coeff_prod_X_pow`, `instIsPushout`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `MvPolynomial.pointToPoint_zeroLocus_le`, `instIsPushout'`, `Algebra.Generators.toAlgHom_ofComp_rename`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply`, `MvPolynomial.derivation_C`, `Algebra.Generators.σ_smul`, `MvPolynomial.mkDerivation_monomial`, `Algebra.Generators.comp_localizationAway_ker`, `MvPolynomial.prime_C_iff`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `Algebra.PreSubmersivePresentation.aevalDifferential_single`, `MvPolynomial.aeval_id_rename`, `MvPolynomial.vars_prod`, `MvPolynomial.sumToIter_iterToSum`, `MvPolynomial.prod_X_pow_eq_monomial`, `MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap`, `MvPolynomial.frobenius_zmod`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `MvPolynomial.pderiv_C_mul`, `Polynomial.homogenize_finsetProd`, `ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial`, `Algebra.Generators.self_algebra_smul`, `MvPolynomial.comap_C_surjective`, `MvPolynomial.eval₂_eta`, `MvPolynomial.finSuccEquiv_eq`, `MvPolynomial.ker_eval₂Hom_universalFactorizationMap`, `MvPolynomial.monomial_sum_index`, `MvPolynomial.degrees_prod_le`, `MvPolynomial.monic_monomial_eq`, `MvPolynomial.pderiv_monomial_single`, `MvPolynomial.degreeOf_prod_eq`, `MvPolynomial.IsHomogeneous.aeval`, `MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse`, `MvPolynomial.pderiv_X_of_ne`, `MvPolynomial.prod_X_add_C_coeff`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `MvPolynomial.pderiv_monomial`, `MonomialOrder.degree_prod_le`, `MvPolynomial.aeval_eq_bind₁`, `MvPolynomial.IsWeightedHomogeneous.prod`, `Algebra.Generators.repr_CotangentSpaceMap`, `DividedPowerAlgebra.dp_sum_smul`, `MvPolynomial.pderiv_pow`, `MvPowerSeries.algebraMap_apply'`, `witt_structure_prop`, `MvPolynomial.eval₂Hom_eq_bind₂`, `MvPolynomial.prod_C_add_X_eq_sum_esymm`, `MvPolynomial.eval₂_map_comp_C`, `MvPolynomial.optionEquivRight_apply`, `MvPolynomial.finSuccEquiv_apply`, `DividedPowerAlgebra.dp_sum`, `MvPolynomial.sumAlgEquiv_apply`, `Algebra.Generators.ker_comp_eq_sup`, `MvPolynomial.sumToIter_Xr`, `MvPolynomial.esymmAlgHom_apply`, `MvPolynomial.monomial_eq`, `MvPolynomial.rename_prod_mk_eval₂`, `MvPolynomial.pderiv_map`, `MvPolynomial.pderiv_inr_universalFactorizationMap_X`, `MvPolynomial.sumAlgEquiv_symm_apply`, `MvPolynomial.instIsPushout_1`, `MvPolynomial.C_mem_pow_idealOfVars_iff`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `MvPolynomial.pderiv_eq_zero_of_notMem_vars`, `MvPolynomial.aeval_C_comp_left`, `MvPolynomial.mapAlgHom_apply`, `Algebra.Generators.cotangentRestrict_mk`, `Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `MvPolynomial.optionEquivLeft_symm_apply`, `MvPolynomial.isLocalization_C_mk'`, `MvPolynomial.eval₂Hom_id_X_eq_join₂`, `Algebra.Generators.Hom.comp_val`, `MvPolynomial.instIsPushout`, `MvPolynomial.esymm_eq_multiset_esymm`, `MvPolynomial.isLocalization`, `MvPolynomial.aeval_id_eq_join₁`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors`, `MonomialOrder.degree_prod`, `ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial`, `MvPolynomial.prod_X_pow`, `MvPolynomial.universalFactorizationMapPresentation_algebra_smul`, `MvPolynomial.IsHomogeneous.sum_X_mul_pderiv`, `MvPolynomial.derivation_C_mul`, `MvPolynomial.aeval_sumElim_pderiv_inl`, `MvPolynomial.iterToSum_C_C`, `MvPolynomial.eval₂_C_mk_eq_zero`, `MvPolynomial.universalFactorizationMap_freeMonic`, `MvPolynomial.universalFactorizationMapPresentation_val`, `MvPolynomial.coe_expand`, `MvPolynomial.aeval_sumElim`, `MvPolynomial.universalFactorizationMapPresentation_σ'`, `AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `MvPolynomial.monomial_sum_one`, `Algebra.Presentation.quotientEquiv_mk`, `sup_support_finset_prod_le`, `MvPolynomial.IsHomogeneous.prod`, `MvPolynomial.degreeOf_prod_le`, `MonomialOrder.sPolynomial_mem_sup_ideal`, `LaurentPolynomial.isLocalization`, `MvPolynomial.join₂_map`, `MvPolynomial.eval₂Hom_C_left`, `MvPolynomial.transcendental_supported_polynomial_aeval_X_iff`, `Algebra.Generators.self_algebra_algebraMap`, `MvPolynomial.esymm_eq_sum_subtype`, `MonomialOrder.Monic.prod`, `MvPolynomial.ringKrullDim_of_isNoetherianRing`, `MvPolynomial.pderiv_X_self`, `MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse`, `le_inf_support_finset_prod`, `MvPolynomial.pderiv_C`, `MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul`, `MvPolynomial.aeval_prod`, `Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `le_inf_support_multiset_prod`, `SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial`, `MvPolynomial.sumToIter_C`, `MvPolynomial.derivation_eqOn_supported`, `MvPolynomial.IsHomogeneous.eval₂`, `MonomialOrder.degree_prod_of_regular`, `MvPolynomial.transcendental_supported_X`, `MvPolynomial.eval₂_assoc`, `DividedPowerAlgebra.prod_dp`, `supDegree_prod_le`, `MvPolynomial.eval_assoc`, `MvPolynomial.vanishingIdeal_zeroLocus_eq_radical`, `rank_mvPolynomial_mvPolynomial`, `MvPolynomial.algebraMap_def`, `Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det`, `MvPolynomial.derivation_ext_iff`, `ringKrullDim_mvPolynomial_of_isEmpty`, `MvPolynomial.IsHomogeneous.pderiv`, `Algebra.SubmersivePresentation.basisDeriv_apply`, `MvPolynomial.bind₁_monomial`, `MvPolynomial.mem_image_comap_C_basicOpen`, `instIsPushoutFractionRingMvPolynomial_1`, `MonomialOrder.degree_prod_of_mem_nonZeroDivisors`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `MvPolynomial.commAlgEquiv_C_X`, `vaddAssocClass_addMonoidAlgebra`, `MvPolynomial.transcendental_supported_polynomial_aeval_X`, `instIsPushoutFractionRingMvPolynomial`, `MvPolynomial.sumToIter_Xl`, `MvPolynomial.pderiv_inl_universalFactorizationMap_X`, `MvPolynomial.instFaithfulSMul`
`curryRingEquiv` 📖	CompOp	2 math math: `curryRingEquiv_symm_single`, `curryRingEquiv_single`
`distribSMul` 📖	CompOp	—
`erase` 📖	CompOp	7 math math: `ofCoeff_erase`, `erase_zero`, `erase_single`, `Polynomial.ofFinsupp_erase`, `Polynomial.toFinsupp_erase`, `coeff_erase`, `Polynomial.erase_def`
`inhabited` 📖	CompOp	—
`instCoeFun` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	2 math math: `MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum`, `MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum`
`instMul` 📖	CompOp	312 math math: `sup_support_list_prod_le`, `instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums`, `MvPolynomial.eval₂_mul_eq_zero_of_left`, `instIsCancelAddZeroOfIsCancelAddOfUniqueSums`, `mul_single_apply`, `LaurentPolynomial.degree_C_mul_T_ite`, `MonomialOrder.sPolynomial_leadingTerm_mul'`, `MvPolynomial.support_mul`, `mapDomainRingEquiv_apply`, `MvPolynomial.mul_X_divMonomial`, `mul_apply`, `LaurentPolynomial.mk'_mul_T`, `liftNC_mul`, `LaurentPolynomial.mul_T_assoc`, `Algebra.Generators.H1Cotangent.δAux_mul`, `MvPolynomial.mapEquiv_symm`, `MvPolynomial.coeff_X_mul'`, `LaurentPolynomial.commute_T`, `MvPolynomial.isEmptyRingEquiv_apply`, `Algebra.Generators.toAlgHom_ofComp_localizationAway`, `LaurentPolynomial.T_sub`, `MvPolynomial.leibniz_iff_X`, `MvPolynomial.divMonomial_add_modMonomial`, `Algebra.Presentation.localizationAway_relation`, `MvPolynomial.monomial_finsupp_sum_index`, `MvPolynomial.coeffs_mul_X`, `MvPolynomial.mul_def`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C`, `MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply`, `MonomialOrder.leadingCoeff_mul_of_isRegular_right`, `Monic.supDegree_mul`, `MvPolynomial.irreducible_mul_X_add`, `MonomialOrder.leadingCoeff_mul`, `WittVector.mul_polyOfInterest_aux2`, `Monic.supDegree_mul_of_ne_zero_right`, `instNoZeroDivisorsOfUniqueSums`, `MvPolynomial.pderiv_mul`, `MvPolynomial.degreeOf_mul_le`, `instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums`, `MvPolynomial.IsWeightedHomogeneous.mul`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `MvPolynomial.X_mul_cancel_right_iff`, `uniqueRingEquiv_apply`, `MvPolynomial.mvPolynomialEquivMvPolynomial_apply`, `opRingEquiv_symm_single`, `opRingEquiv_symm_apply`, `MvPolynomial.eval₂_mul_monomial`, `MonomialOrder.div_single`, `MvPolynomial.esymmAlgHomMonomial_single`, `MvPolynomial.homogeneousComponent_C_mul`, `LaurentPolynomial.eval₂_C_mul_T`, `Polynomial.toLaurent_C_mul_T`, `LaurentPolynomial.invOf_T`, `MvPolynomial.monomial_mul_mem_coeffsIn`, `MvPolynomial.X_mul_pderiv_monomial`, `supDegree_mul`, `MvPolynomial.totalDegree_list_prod`, `LaurentPolynomial.smeval_C_mul`, `of'_commute`, `WeierstrassCurve.Jacobian.polynomialY_eq`, `single_commute_single`, `of'_mul_divOf`, `MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors`, `MvPolynomial.mul_X_mem_coeffsIn`, `MvPolynomial.totalDegree_mul_of_isDomain`, `MvPolynomial.X_mul_mem_coeffsIn`, `MonomialOrder.degree_mul_leadingTerm`, `xInTermsOfW_eq`, `Monic.leadingCoeff_mul_eq_left`, `MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul`, `LaurentPolynomial.degree_C_mul_T`, `support_mul_single_subset`, `MvPolynomial.C_mul_X_eq_monomial`, `MvPolynomial.degreeOf_mul_eq`, `MvPolynomial.bind₂_monomial`, `Algebra.SubmersivePresentation.jacobianRelations_spec`, `WeierstrassCurve.Projective.polynomialZ_eq`, `Monic.mul`, `support_single_mul_subset`, `MvPolynomial.coeff_C_mul`, `MvPolynomial.C_mul_monomial`, `MvPolynomial.mapEquiv_apply`, `toDirectSum_mul`, `wittPolynomial_one`, `MvPolynomial.eval₂_mul_eq_zero_of_right`, `IsLocalization.Away.mvPolynomialQuotientEquiv_apply`, `mul_def`, `MvPolynomial.isHomogeneous_C_mul_X`, `WittVector.mul_polyOfInterest_aux4`, `LaurentPolynomial.mk'_eq`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `Algebra.Generators.localizationAway_σ`, `MvPolynomial.IsSymmetric.mul`, `MonomialOrder.degree_mul_of_isRegular_right`, `Monic.leadingCoeff_mul_eq_right`, `MvPolynomial.coeff_monomial_mul`, `MvPolynomial.X_mul_cancel_left_iff`, `MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero`, `MvPolynomial.X_dvd_mul_iff`, `MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv`, `MvPolynomial.isEmptyRingEquiv_symm_apply`, `MonomialOrder.degree_leadingTerm_mul`, `apply_add_of_supDegree_le`, `DirectSum.toAddMonoidAlgebra_mul`, `MvPolynomial.modMonomial_add_divMonomial`, `WittVector.bind₁_wittMulN_wittPolynomial`, `commRingEquiv_single_single`, `MvPolynomial.dvd_X_mul_iff`, `mul_of'_modOf`, `MvPolynomial.monomial_one_mul_cancel_left_iff`, `MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul`, `xInTermsOfW_aux`, `MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero`, `mul_single_zero_apply`, `MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff`, `le_inf_support_list_prod`, `MonomialOrder.toSyn_degree_mul_le`, `Polynomial.homogenize_X_pow`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `wittStructureRat_rec`, `WittVector.mul_polyOfInterest_vars`, `MvPolynomial.isRegular_prod_X`, `MonomialOrder.degree_mul_le`, `MonomialOrder.sPolynomial_def`, `MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors`, `MvPolynomial.monomial_add_single`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none`, `MvPolynomial.instNoZeroDivisors`, `MvPolynomial.coeff_monomial_mul'`, `MvPolynomial.vars_C_mul`, `wittStructureRat_rec_aux`, `Algebra.Generators.ker_localizationAway`, `MvPolynomial.support_mul_X`, `mapDomainRingEquiv_trans`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply`, `support_mul_single_eq_image`, `MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors`, `mul_apply_left`, `Algebra.Generators.comp_localizationAway_ker`, `MvPolynomial.mul_esymm_eq_sum`, `MvPolynomial.eval_mul`, `single_zero_comm`, `MvPolynomial.degreeOf_mul_X_self`, `WeierstrassCurve.Projective.polynomialX_eq`, `modOf_add_divOf`, `Polynomial.homogenize_C_mul`, `MvPolynomial.divMonomial_mul_monomial`, `LaurentPolynomial.eval₂_C_mul_T_neg_n`, `WeierstrassCurve.Projective.polynomialY_eq`, `support_mul`, `Polynomial.toFinsupp_mul`, `MvPolynomial.coeff_mul_X'`, `MvPolynomial.coeff_mul_X`, `WittVector.frobeniusPolyAux_eq`, `single_mul_apply`, `MvPolynomial.C_mul'`, `Algebra.Generators.cMulXSubOneCotangent_eq`, `MvPolynomial.pderiv_C_mul`, `mapRingEquiv_apply`, `MvPolynomial.eval₂_mul`, `single_mul_apply_of_not_exists_add`, `LaurentPolynomial.single_eq_C_mul_T`, `MvPolynomial.X_mul_divMonomial`, `Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs`, `WeierstrassCurve.Jacobian.polynomialZ_eq`, `MonomialOrder.sPolynomial_monomial_mul`, `MvPolynomial.isRegular_X`, `MvPolynomial.monomial_sum_index`, `opRingEquiv_single`, `ofMagma_apply`, `mul_single_apply_aux`, `sup_support_mul_le`, `MvPolynomial.isEmptyRingEquiv_symm_toRingHom`, `WittVector.mul_polyOfInterest_aux1`, `MvPolynomial.monomial_mul`, `mul_apply_add_eq_mul_of_uniqueAdd`, `single_mul_single`, `MvPolynomial.isRegular_X_pow`, `le_infDegree_mul`, `MvPolynomial.degrees_mul_le`, `le_inf_support_mul`, `MvPolynomial.dvd_monomial_mul_iff_exists`, `curryRingEquiv_symm_single`, `opRingEquiv_apply`, `MonomialOrder.div_set`, `mapDomainRingEquiv_single`, `MvPolynomial.X_mul_modMonomial`, `Monic.supDegree_mul_of_ne_zero_left`, `MvPolynomial.pderiv_pow`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `MvPolynomial.tensorEquivSum_X_tmul_X`, `Polynomial.toFinsuppIso_apply`, `MvPolynomial.vars_mul`, `Algebra.Presentation.relation_comp_localizationAway_inl`, `uniqueRingEquiv_symm_apply`, `leadingCoeff_mul`, `MvPolynomial.degreeOf_mul_C_le`, `mapDomain_mul`, `MvPolynomial.esymmAlgHomMonomial_add`, `MvPolynomial.degrees_mul_eq`, `MvPolynomial.isHomogeneous_C_mul_X_pow`, `Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one`, `MvPolynomial.degreeOf_C_mul_le`, `symm_mapDomainRingEquiv`, `MvPolynomial.monomial_eq`, `LaurentPolynomial.counit_C_mul_T`, `WittVector.wittMul_zero`, `MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc'`, `MvPolynomial.eval₂_mul_C`, `MvPolynomial.instIsCancelMulZeroOfIsCancelAdd`, `WittVector.polyOfInterest_vars_eq`, `MvPolynomial.mapEquiv_trans`, `supDegree_mul_le`, `MvPolynomial.IsHomogeneous.mul`, `divOf_add_modOf`, `MvPolynomial.weightedHomogeneousComponent_C_mul`, `Polynomial.ofFinsupp_mul`, `MvPolynomial.mul_monomial_mem_coeffsIn`, `MonomialOrder.sPolynomial_monomial_mul'`, `WeierstrassCurve.Jacobian.polynomialX_eq`, `MvPolynomial.C_mul_X_pow_eq_monomial`, `MvPolynomial.totalDegree_mul`, `MvPolynomial.psum_eq_mul_esymm_sub_sum`, `MvPolynomial.IsWeightedHomogeneous.C_mul`, `support_single_mul`, `MonomialOrder.leadingCoeff_mul_of_isRegular_left`, `support_single_mul_eq_image`, `MvPolynomial.degreeOf_C_mul`, `MvPolynomial.C_mul`, `LaurentPolynomial.support_C_mul_T_of_ne_zero`, `single_zero_mul_apply`, `MvPolynomial.divMonomial_monomial_mul`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `MvPolynomial.coeff_mul_monomial`, `IsRegular.monomial`, `MvPolynomial.divMonomial_add_modMonomial_single`, `MvPolynomial.smul_eq_C_mul`, `LaurentPolynomial.comul_C_mul_T`, `LaurentPolynomial.smeval_C_mul_T_n`, `MvPolynomial.IsHomogeneous.sum_X_mul_pderiv`, `MvPolynomial.mul_monomial_modMonomial`, `MvPolynomial.mapEquiv_refl`, `MvPolynomial.coeff_X_mul`, `single_mul_apply_aux`, `Polynomial.toFinsuppIso_symm_apply`, `LaurentPolynomial.smul_eq_C_mul`, `MonomialOrder.degree_mul_of_isRegular_left`, `Polynomial.toLaurent_C_mul_eq`, `MonomialOrder.Monic.mul`, `Polynomial.homogenize_C`, `curryRingEquiv_single`, `MonomialOrder.div`, `WittVector.mul_polyOfInterest_aux5`, `addMonoidAlgebraRingEquivDirectSum_apply`, `MvPolynomial.mul_X_modMonomial`, `LaurentPolynomial.trunc_C_mul_T`, `LaurentPolynomial.support_C_mul_T`, `Polynomial.homogenize_X`, `MonomialOrder.coeff_mul_of_degree_add`, `MonomialOrder.coeff_mul_of_add_of_degree_le`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`, `StandardEtalePresentation.toPresentation_relation`, `MonomialOrder.degree_mul`, `MvPolynomial.coeff_mul_monomial'`, `WittVector.mul_polyOfInterest_aux3`, `of'_mul_modOf`, `MvPolynomial.modMonomial_add_divMonomial_single`, `MvPowerSeries.trunc_C_mul`, `MvPolynomial.isEmptyRingEquiv_eq_coeff_zero`, `symm_mapRingEquiv`, `symm_commRingEquiv`, `Polynomial.toLaurent_C_mul_X_pow`, `LaurentPolynomial.eval₂_C_mul_T_n`, `LaurentPolynomial.toLaurent_reverse`, `MvPolynomial.IsHomogeneous.C_mul`, `single_commute`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `MonomialOrder.C_mul_leadingCoeff_monomial_degree`, `MvPolynomial.degreeOf_mul_X_of_ne`, `Algebra.Generators.comp_σ`, `LaurentPolynomial.comul_C_mul_T_self`, `mul_apply_right`, `LaurentPolynomial.T_add`, `MvPolynomial.monomial_single_add`, `wittPolynomial_eq_sum_C_mul_X_pow`, `MvPolynomial.support_X_mul`, `MvPolynomial.monomial_one_mul_cancel_right_iff`, `MonomialOrder.degree_mul'`, `Polynomial.homogenize_mul`, `LaurentPolynomial.exists_T_pow`, `mul_single_apply_of_not_exists_add`, `MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero`, `MvPolynomial.coeffs_X_mul`, `MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors`, `support_mul_single`, `LaurentPolynomial.antipode_C_mul_T`, `MvPolynomial.coeff_mul`, `mapRingEquiv_trans`, `MvPolynomial.bind₁_monomial`, `MvPolynomial.coe_mul`, `map_mul`, `mapRingEquiv_single`, `mul_apply_antidiagonal`, `MonomialOrder.sPolynomial_mul_monomial`, `LaurentPolynomial.degree_C_mul_T_le`, `Algebra.Generators.C_mul_X_sub_one_mem_ker`, `MonomialOrder.sPolynomial_leadingTerm_mul`, `MvPowerSeries.trunc'_C_mul`, `LaurentPolynomial.T_mul`, `apply_supDegree_add_supDegree`, `MvPolynomial.monomial_mul_modMonomial`, `mul_of'_divOf`
`nonAssocRing` 📖	CompOp	2 math math: `intCast_def`, `supDegree_sub_lt_of_leadingCoeff_eq`
`nonAssocSemiring` 📖	CompOp	572 math math: `MvPolynomial.is_id`, `MvPolynomial.funext_iff`, `MvPolynomial.eval_indicator_apply_eq_one`, `Height.logHeight_eval_ge`, `singleHom_apply`, `LaurentPolynomial.degree_C_mul_T_ite`, `MvPolynomial.coe_C`, `MvPolynomial.map_bind₁`, `Polynomial.toLaurent_eq_zero`, `MvPolynomial.map_mapRange_eq_iff`, `MvPolynomial.map_comp_C`, `MvPolynomial.eval₂Hom_X`, `algHom_ext'_iff`, `MvPolynomial.toMvPowerSeries_uniformContinuous`, `MonomialOrder.monic_X_sub_C`, `MvPolynomial.hom_C`, `Polynomial.homogenize_map`, `Ideal.mem_span_iff_exists_isHomogeneous`, `LaurentPolynomial.mk'_mul_T`, `WeierstrassCurve.Projective.eval_polynomial`, `MvPolynomial.universalFactorizationMap_comp_map`, `liftNCRingHom_single`, `MvPolynomial.IsSymmetric.map`, `MvPolynomial.isEmptyRingEquiv_apply`, `MvPolynomial.ker_map`, `MvPolynomial.map_leftInverse`, `MvPolynomial.optionEquivLeft_C`, `MvPolynomial.iterToSum_sumToIter`, `constantCoeff_wittStructureRat`, `Algebra.Generators.toAlgHom_ofComp_localizationAway`, `MvPolynomial.eval₂Hom_monomial`, `WeierstrassCurve.Jacobian.baseChange_polynomialZ`, `Algebra.Presentation.localizationAway_relation`, `MvPolynomial.monomial_finsupp_sum_index`, `MvPolynomial.bind₂_comp_C`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C`, `MvPolynomial.eval₂_zero'_apply`, `MvPolynomial.degreeOf_C`, `WeierstrassCurve.Projective.polynomial_relation`, `MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply`, `AlgebraicIndependent.repr_ker`, `MvPolynomial.mem_range_map_iff_coeffs_subset`, `MvPolynomial.exists_dvd_map_of_isAlgebraic`, `AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin`, `AnalyticOnNhd.eval_linearMap'`, `MvPolynomial.bind₂_C_left`, `MvPolynomial.map_comp_rename`, `Polynomial.eval_eq_div_eval_toTupleMvPolynomial`, `WeierstrassCurve.Jacobian.eval_polynomialY`, `MvPolynomial.constantCoeff_rename`, `MvPolynomial.map_bind₂`, `MvPolynomial.iterToSum_C_X`, `MvPolynomial.map_eval₂`, `MvPolynomial.eval_map`, `MvPolynomial.map_eval₂Hom`, `toRingHom_mapDomainRingEquiv`, `char_dvd_card_solutions_of_add_lt`, `MvPolynomial.comp_eval₂Hom`, `lift_mapRangeRingHom_algebraMap`, `MvPolynomial.aeval_eq_eval`, `MvPolynomial.schwartz_zippel_totalDegree`, `Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs`, `MvPolynomial.eval₂Hom_C_id_eq_join₁`, `MvPolynomial.eval_mem`, `ax_grothendieck_of_definable`, `MvPolynomial.join₂_comp_map`, `Height.logHeight_eval_ge'`, `divOfHom_apply_apply`, `MvPolynomial.eval_rename_prod_mk`, `MvPolynomial.optionEquivRight_C`, `MvPolynomial.map_mvPolynomial_eq_eval₂`, `MvPolynomial.eval_eval₂`, `MvPolynomial.aevalTower_comp_C`, `Polynomial.trunc_toLaurent`, `MvPolynomial.eval₂_id`, `MvPolynomial.eval₂Hom_C_eq_bind₁`, `toRingHom_mapAlgHom`, `MvPolynomial.constantCoeff_C`, `MvPowerSeries.trunc_C`, `MvPolynomial.map_map`, `MvPolynomial.eval₂Hom_comp_bind₂`, `MvPolynomial.mvPolynomialEquivMvPolynomial_apply`, `MvPolynomial.weightedHomogeneousComponent_zero`, `MvPolynomial.esymmAlgHomMonomial_single`, `MvPolynomial.homogeneousComponent_C_mul`, `Polynomial.ofFinsupp_natCast`, `LaurentPolynomial.eval₂_C_mul_T`, `Polynomial.toLaurent_C_mul_T`, `MvPolynomial.IsHomogeneous.map`, `MvPolynomial.map_expand`, `MvPolynomial.map_aeval`, `MvPolynomial.map_frobenius_expand`, `Height.logHeight_eval_le'`, `FirstOrder.Ring.lift_genericPolyMap`, `MvPolynomial.expand_char`, `MvPolynomial.eval₂Hom_congr`, `WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero`, `mapRingHom_id`, `MvPolynomial.map_rename`, `MvPolynomial.killCompl_C`, `singleZeroRingHom_apply`, `LaurentPolynomial.algebraMap_apply`, `MvPolynomial.eval_comp_toMvPolynomial`, `Algebra.Generators.H1Cotangent.δAux_C`, `Algebra.Generators.ofComp_val`, `Algebra.Presentation.map_relationOfHasCoeffs`, `MvPolynomial.eval₂_map`, `MvPolynomial.X_mul_pderiv_monomial`, `MvPolynomial.map_esymm`, `mapDomainRingHom_comp_algebraMap`, `MvPolynomial.expand_C`, `LaurentPolynomial.smeval_C_mul`, `MonomialOrder.eq_C_of_degree_eq_zero`, `MvPolynomial.coeffs_C`, `MvPolynomial.optionEquivRight_X_none`, `WeierstrassCurve.Jacobian.polynomialY_eq`, `WeierstrassCurve.Jacobian.eval_polynomialX`, `MvPolynomial.C_apply`, `Polynomial.toLaurent_injective`, `WeierstrassCurve.Projective.eval_polynomialX`, `WeierstrassCurve.Projective.baseChange_polynomial`, `of_apply`, `Matrix.toMvPolynomial_map`, `MvPolynomial.coeff_C`, `WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero`, `MvPolynomial.bind₂_map`, `constantCoeff_wittStructureInt`, `MvPolynomial.eval_ofNat`, `xInTermsOfW_eq`, `MvPolynomial.eval_eq_eval_mv_eval'`, `MvPolynomial.degrees_map_of_injective`, `MvPolynomial.ACounit_C`, `LaurentPolynomial.degree_C_mul_T`, `mapRingHom_comp_algebraMap`, `MvPolynomial.eval₂Hom_zero_apply`, `MvPolynomial.degrees_C`, `WeierstrassCurve.Jacobian.polynomial_relation`, `MvPolynomial.eval_prod`, `MvPolynomial.C_mul_X_eq_monomial`, `Algebra.Presentation.comp_aeval_relation_inl`, `MvPolynomial.C_0`, `LaurentPolynomial.smeval_C`, `MvPolynomial.bind₂_monomial`, `isLocalHom_singleZeroRingHom`, `MvPolynomial.monomialOneHom_apply`, `MvPolynomial.pderiv_sumToIter`, `MvPolynomial.totalDegree_C`, `ringHom_ext'_iff`, `WeierstrassCurve.Projective.polynomialZ_eq`, `LaurentPolynomial.degree_C`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'`, `MvPolynomial.coeff_C_mul`, `LaurentPolynomial.eval₂_T`, `MvPolynomial.quotient_map_C_eq_zero`, `MvPolynomial.iterToSum_X`, `MvPolynomial.C_mul_monomial`, `AnalyticOnNhd.eval_linearMap`, `LaurentPolynomial.C_apply`, `MvPolynomial.commAlgEquiv_C`, `MvPolynomial.coeff_zero_C`, `MonomialOrder.monic_X_add_C`, `MvPolynomial.bind₂_monomial_one`, `MvPolynomial.commAlgEquiv_X`, `MvPolynomial.mapEquiv_apply`, `MvPolynomial.eval₂Hom_congr'`, `Matrix.charpoly.univ_coeff_eval₂Hom`, `Polynomial.toFinsupp_nsmul`, `MvPolynomial.instCharZero`, `MvPolynomial.C_1`, `MvPolynomial.eval₂Hom_X'`, `IsNonarchimedean.eval_mvPolynomial_le`, `Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs`, `wittPolynomial_one`, `Polynomial.toLaurent_comp_C`, `MvPolynomial.eval_eq'`, `MvPolynomial.eval₂_C`, `IsLocalization.Away.mvPolynomialQuotientEquiv_apply`, `MvPolynomial.C_add`, `MvPolynomial.isHomogeneous_C_mul_X`, `LaurentPolynomial.mk'_eq`, `Algebra.Generators.localizationAway_σ`, `MvPolynomial.mapAlgEquiv_apply`, `WittVector.frobeniusPoly_zmod`, `MvPolynomial.eval_neg`, `MvPolynomial.tensorEquivSum_one_tmul_C`, `toDirectSum_natCast`, `WeierstrassCurve.Jacobian.baseChange_polynomialY`, `MvPolynomial.map_ofNat`, `MvPolynomial.eval₂Hom_rename`, `MvPolynomial.bind₂_id`, `WeierstrassCurve.Projective.baseChange_polynomialY`, `MvPolynomial.algebraMap_apply`, `LinearMap.toMvPolynomial_baseChange`, `MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv`, `MvPowerSeries.truncFinset_C`, `MvPolynomial.C_surjective`, `MvPolynomial.isEmptyRingEquiv_symm_apply`, `Polynomial.toLaurent_apply`, `MvPolynomial.hom_eq_hom`, `Polynomial.eval_homogenize`, `MvPolynomial.bind₁_C_right`, `MvPolynomial.coe_coeffs_map`, `MvPowerSeries.truncFinset_map`, `MonomialOrder.degree_X_sub_C`, `MvPolynomial.aevalTower_C`, `MvPolynomial.map_expand_pow_char`, `xInTermsOfW_aux`, `MvPolynomial.mapRange_eq_map`, `MvPolynomial.totalDegree_eq_zero_iff_eq_C`, `WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero`, `MvPolynomial.eval₂Hom_zero'`, `Polynomial.Bivariate.equivMvPolynomial_symm_C`, `MvPolynomial.map_hsymm`, `coe_mapRingHom`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `wittStructureRat_rec`, `DirectSum.toAddMonoidAlgebra_natCast`, `MvPolynomial.expand_eq_C`, `MvPolynomial.degrees_map_le`, `LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff`, `MvPolynomial.eval_eq`, `LaurentPolynomial.algebraMap_eq_toLaurent`, `MvPolynomial.isUnit_iff_eq_C_of_isReduced`, `MvPolynomial.psum_zero`, `Polynomial.toLaurent_X_pow`, `MvPolynomial.eval_add`, `WeierstrassCurve.Projective.map_polynomialX`, `Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs`, `MvPowerSeries.trunc_map`, `WeierstrassCurve.Jacobian.baseChange_polynomial`, `MvPolynomial.eval_monomial`, `MonomialOrder.degree_C`, `MvPolynomial.coe_eval₂Hom`, `MvPolynomial.vars_C_mul`, `AbsoluteValue.eval_mvPolynomial_le`, `Algebra.Generators.toAlgHom_ofComp_rename`, `Polynomial.toFinsupp_natCast`, `wittStructureRat_rec_aux`, `WeierstrassCurve.Projective.eval_polynomialZ`, `Algebra.Generators.ker_localizationAway`, `MvPolynomial.constantCoeff_smul`, `MvPolynomial.algHom_C`, `mapDomainRingHom_comp`, `MvPolynomial.leadingCoeff_toLex_C`, `MvPolynomial.eval_pow`, `MvPolynomial.eval₂Hom_zero'_apply`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply`, `LaurentPolynomial.single_eq_C`, `MvPolynomial.derivation_C`, `Height.mulHeight_eval_ge`, `MvPolynomial.dvd_smul_X_iff_exists`, `MvPolynomial.schwartz_zippel_sup_sum`, `MvPolynomial.mem_map_C_iff`, `MvPolynomial.prime_C_iff`, `MvPolynomial.eval_mul`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `MvPolynomial.aevalTower_comp_algebraMap`, `MvPolynomial.eval₂_zero_apply`, `MonomialOrder.monic_C_one`, `MvPolynomial.eq_C_of_isEmpty`, `toRingHom_mapRingEquiv`, `WeierstrassCurve.Projective.polynomialX_eq`, `MvPolynomial.monomial_zero'`, `Polynomial.homogenize_C_mul`, `mapRingHom_single`, `natCast_def`, `MvPolynomial.eval_indicator_apply_eq_zero`, `MvPolynomial.sumToIter_iterToSum`, `MvPolynomial.map_surjective_iff`, `LaurentPolynomial.eval₂_C_mul_T_neg_n`, `constantCoeff_wittPolynomial`, `WeierstrassCurve.Projective.polynomialY_eq`, `MvPolynomial.aeval_eq_constantCoeff_of_vars`, `lift_of`, `WeierstrassCurve.Projective.negDblY_eq`, `MvPolynomial.map_injective_iff`, `MvPolynomial.map_injective`, `MvPolynomial.constantCoeff_monomial`, `MvPolynomial.smul_eval`, `MvPolynomial.eval₂Hom_zero`, `MvPolynomial.C_eq_zero`, `MvPolynomial.supDegree_toLex_C`, `WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero`, `MvPolynomial.aeval_zero`, `MvPolynomial.hom_congr_vars`, `MvPolynomial.support_map_of_injective`, `MvPolynomial.constantCoeff_X`, `WittVector.frobeniusPolyAux_eq`, `LaurentPolynomial.C_eq_algebraMap`, `WeierstrassCurve.Projective.baseChange_polynomialX`, `MvPolynomial.C_mul'`, `MvPolynomial.isEmptyAlgEquiv_apply`, `MvPolynomial.bind₂_X_right`, `Algebra.Generators.cMulXSubOneCotangent_eq`, `MvPolynomial.map_C`, `MvPolynomial.C_dvd_iff_dvd_coeff`, `MvPolynomial.pderiv_C_mul`, `Matrix.toMvPolynomial_eval_eq_apply`, `LaurentPolynomial.single_eq_C_mul_T`, `WittVector.constantCoeff_wittMul`, `LaurentPolynomial.comul_C`, `MvPolynomial.funext_set_iff`, `MvPolynomial.map_monomial`, `MvPolynomial.vars_map_of_injective`, `MvPolynomial.aeval_map_algebraMap`, `Algebra.Generators.Hom.toAlgHom_C`, `LaurentPolynomial.eval₂_C`, `MvPolynomial.finSuccEquiv_comp_C_eq_C`, `MvPolynomial.esymmAlgHom_zero`, `char_dvd_card_solutions`, `WeierstrassCurve.Jacobian.polynomialZ_eq`, `MvPolynomial.eval₂Hom_map_hom`, `LaurentPolynomial.eval₂_toLaurent`, `MvPolynomial.finSuccEquiv_eq`, `char_dvd_card_solutions_of_sum_lt`, `lift_unique'`, `RingHom.IsStandardSmooth.exists_etale_mvPolynomial`, `MvPolynomial.homogeneousComponent_zero`, `MvPolynomial.ker_eval₂Hom_universalFactorizationMap`, `MvPolynomial.coeff_map`, `MvPolynomial.monomial_sum_index`, `Matrix.mvPolynomialX_mapMatrix_eval`, `MonomialOrder.degree_eq_zero_iff`, `MvPolynomial.isEmptyRingEquiv_symm_toRingHom`, `MonomialOrder.leadingTerm_C`, `MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse`, `Height.mulHeight_eval_le`, `MvPolynomial.aeval_bind₂`, `LaurentPolynomial.toLaurent_support`, `MvPolynomial.counit_surjective`, `WeierstrassCurve.Projective.negDblY_eq'`, `LinearMap.polyCharpolyAux_coeff_eval`, `MvPolynomial.map_rightInverse`, `MvPolynomial.killCompl_map`, `MvPolynomial.dvd_X_iff_exists`, `MvPolynomial.eval₂Hom_eq_zero`, `MvPolynomial.instCharP`, `MonomialOrder.leadingCoeff_C`, `MvPolynomial.ker_mapAlgHom`, `WittVector.constantCoeff_wittAdd`, `MvPolynomial.eval_sub`, `Height.logHeight_eval_le`, `MvPolynomial.pderiv_pow`, `constantCoeff_wittStructureRat_zero`, `WeierstrassCurve.Jacobian.map_polynomialZ`, `MvPolynomial.bind₂_C_right`, `MvPolynomial.constantCoeff_eq`, `LinearMap.toMvPolynomial_constantCoeff`, `WeierstrassCurve.Projective.map_polynomialZ`, `MvPolynomial.eval_rename`, `MvPolynomial.mkDerivationₗ_C`, `witt_structure_prop`, `MvPolynomial.map_surjective`, `WittVector.constantCoeff_wittNSMul`, `lift_mapRingHom_algebraMap`, `MvPolynomial.eval₂_map_comp_C`, `MvPolynomial.optionEquivRight_apply`, `MvPolynomial.finSuccEquiv_apply`, `MvPolynomial.C_eq_coe_nat`, `MvPolynomial.bind₂_comp_bind₂`, `WeierstrassCurve.Jacobian.baseChange_polynomialX`, `MvPolynomial.degreeOf_mul_C_le`, `Polynomial.toLaurent_inj`, `MvPolynomial.algebraTensorAlgEquiv_symm_map`, `MvPolynomial.isHomogeneous_C_mul_X_pow`, `MvPolynomial.tensorEquivSum_C_tmul_one`, `MvPolynomial.map_iterateFrobenius_expand`, `MvPolynomial.sumAlgEquiv_apply`, `MvPolynomial.degreeOf_C_mul_le`, `MvPolynomial.sumToIter_Xr`, `WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero`, `MvPolynomial.eval_toMvPolynomial`, `MvPolynomial.sum_C`, `MvPolynomial.monomial_eq`, `LaurentPolynomial.counit_C_mul_T`, `MvPolynomial.aeval_eq_eval₂Hom`, `MvPolynomial.vars_C`, `MvPolynomial.aeval_C`, `MvPolynomial.support_map_subset`, `MvPolynomial.pderiv_map`, `WeierstrassCurve.Jacobian.eval_polynomial`, `Polynomial.toLaurent_one`, `MvPolynomial.rename_C`, `FirstOrder.realize_genericPolyMapSurjOnOfInjOn`, `MvPolynomial.eval₂_mul_C`, `LaurentPolynomial.degree_C_ite`, `MvPolynomial.C_neg`, `LaurentPolynomial.eval₂_T_neg_n`, `MvPolynomial.coeToMvPowerSeries.ringHom_apply`, `MvPolynomial.coeffs_map`, `WeierstrassCurve.Jacobian.map_polynomial`, `MvPolynomial.constantCoeff_comp_C`, `MvPolynomial.sumAlgEquiv_symm_apply`, `MvPolynomial.eval₂_comp`, `MvPolynomial.weightedHomogeneousComponent_C_mul`, `WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero`, `MvPolynomial.dvd_C_iff_exists`, `LaurentPolynomial.antipode_C`, `MvPolynomial.C_mem_pow_idealOfVars_iff`, `of_injective`, `WittVector.map_frobeniusPoly`, `MvPolynomial.sum_eval_eq_zero`, `WittVector.constantCoeff_wittZSMul`, `WeierstrassCurve.Jacobian.polynomialX_eq`, `MvPolynomial.aeval_C_comp_left`, `MvPolynomial.C_mul_X_pow_eq_monomial`, `MvPolynomial.eval_C`, `MvPolynomial.IsWeightedHomogeneous.C_mul`, `MvPolynomial.mapAlgHom_apply`, `map_wittPolynomial`, `MvPolynomial.isLocalization_C_mk'`, `MvPolynomial.algebraTensorAlgEquiv_tmul`, `MvPolynomial.vars_map`, `MvPolynomial.degreeOf_C_mul`, `MvPolynomial.C_injective`, `MvPolynomial.C_mul`, `LaurentPolynomial.support_C_mul_T_of_ne_zero`, `MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars`, `MvPolynomial.isLocalization`, `LaurentPolynomial.counit_C`, `MvPolynomial.instExpChar`, `MvPolynomial.IsSymmetric.C`, `MvPolynomial.ringHom_ext'_iff`, `MvPolynomial.eval_sum`, `MvPolynomial.smul_eq_C_mul`, `MvPolynomial.counitNat_C`, `LaurentPolynomial.comul_C_mul_T`, `Algebra.Presentation.HasCoeffs.relation_mem_range_map`, `LaurentPolynomial.smeval_C_mul_T_n`, `MvPolynomial.IsHomogeneous.sum_X_mul_pderiv`, `MvPolynomial.derivation_C_mul`, `MvPolynomial.aeval_sumElim_pderiv_inl`, `MvPolynomial.eval₂_natCast`, `MvPolynomial.iterToSum_C_C`, `MvPolynomial.totalDegree_sub_C_le`, `MvPolynomial.coeffAddMonoidHom_apply`, `LaurentPolynomial.leftInverse_trunc_toLaurent`, `MvPolynomial.eval₂_C_mk_eq_zero`, `MvPolynomial.aeval_sumElim`, `MvPolynomial.universalFactorizationMapPresentation_σ'`, `LinearMap.toMvPolynomial_eval_eq_apply`, `LaurentPolynomial.smul_eq_C_mul`, `Polynomial.toLaurent_C_mul_eq`, `MvPolynomial.mapAlgHom_coe_ringHom`, `MvPolynomial.schwartz_zippel_sum_degreeOf`, `MvPolynomial.isHomogeneous_C`, `ax_grothendieck_of_locally_finite`, `LaurentPolynomial.eval₂_T_n`, `Polynomial.homogenize_C`, `MvPolynomial.aeval_zero'`, `MvPolynomial.counit_C`, `WeierstrassCurve.Projective.baseChange_polynomialZ`, `MvPolynomial.counitNat_X`, `MonomialOrder.degree_X_add_C`, `MvPolynomial.eval₂Hom_bind₂`, `LaurentPolynomial.trunc_C_mul_T`, `MvPolynomial.bind₂_bind₂`, `LaurentPolynomial.support_C_mul_T`, `MvPolynomial.eval₂Hom_bind₁`, `WeierstrassCurve.Projective.dblX_eq`, `Polynomial.toLaurent_X`, `Algebra.Presentation.baseChange_relation`, `ax_grothendieck_univ`, `MvPolynomial.C_mem_coeffsIn`, `MvPolynomial.join₂_map`, `MvPolynomial.eval₂Hom_C_left`, `Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix`, `MvPolynomial.coeff_eval_eq_eval_coeff`, `mapDomainRingHom_id`, `MvPolynomial.C_pow`, `MvPolynomial.coeffs_C_subset`, `MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing`, `MvPolynomial.C_sub`, `MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse`, `Polynomial.coe_toLaurentAlg`, `MvPolynomial.pderiv_C`, `constantCoeff_xInTermsOfW`, `MvPolynomial.C_dvd_iff_zmod`, `Height.mulHeight_eval_le'`, `MvPowerSeries.trunc_C_mul`, `WittVector.constantCoeff_wittNeg`, `map_wittStructureInt`, `MvPolynomial.constantCoeff_comp_map`, `MvPolynomial.optionEquivLeft_elim_eval`, `MvPolynomial.eval₂Hom_C`, `MvPolynomial.counitNat_surjective`, `MvPolynomial.sumToIter_C`, `Height.mulHeight_eval_ge'`, `WeierstrassCurve.Projective.dblX_eq'`, `MvPolynomial.eval_expand`, `RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`, `Polynomial.toLaurent_C`, `MvPolynomial.supportedEquivMvPolynomial_symm_C`, `Matrix.toMvPolynomial_constantCoeff`, `MvPowerSeries.trunc'_map`, `Polynomial.toLaurentAlg_apply`, `mapRingHom_apply`, `MvPolynomial.eval₂AlgHom_apply`, `MvPolynomial.C_inj`, `WeierstrassCurve.Jacobian.map_polynomialY`, `MvPolynomial.eval_X`, `Ideal.mem_span_pow_iff_exists_isHomogeneous`, `Polynomial.toLaurent_C_mul_X_pow`, `LaurentPolynomial.eval₂_C_mul_T_n`, `WeierstrassCurve.Projective.dblY_of_Y_eq'`, `LaurentPolynomial.toLaurent_reverse`, `MvPolynomial.IsHomogeneous.C_mul`, `MvPolynomial.constantCoeff_map`, `AnalyticOnNhd.eval_continuousLinearMap'`, `MvPolynomial.optionEquivLeft_symm_C_C`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `MonomialOrder.C_mul_leadingCoeff_monomial_degree`, `of'_eq_of`, `AnalyticOnNhd.eval_mvPolynomial`, `mapRingHom_comp`, `WeierstrassCurve.Projective.map_polynomialY`, `MvPolynomial.tensorEquivSum_C_tmul_C`, `WeierstrassCurve.Projective.map_polynomial`, `DividedPowerAlgebra.mkRingHom_C`, `WeierstrassCurve.Projective.eval_polynomialY`, `LaurentPolynomial.comul_C_mul_T_self`, `LaurentPolynomial.instIsScalarTowerPolynomial`, `LaurentPolynomial.invert_C`, `MvPolynomial.instIsLocalHomRingHomC`, `MvPolynomial.eval₂_eq_eval_map`, `Polynomial.Bivariate.equivMvPolynomial_C_C`, `DividedPowerAlgebra.mkAlgHom_C`, `MvPolynomial.isWeightedHomogeneous_C`, `Polynomial.ofFinsupp_nsmul`, `MvPolynomial.map_X`, `MvPolynomial.eval_assoc`, `ax_grothendieck_zeroLocus`, `wittPolynomial_eq_sum_C_mul_X_pow`, `constantCoeff_wittStructureInt_zero`, `MvPolynomial.hom_bind₁`, `WeierstrassCurve.Jacobian.map_polynomialX`, `MvPolynomial.C_dvd_iff_map_hom_eq_zero`, `AnalyticOnNhd.eval_continuousLinearMap`, `WeierstrassCurve.Jacobian.eval_polynomialZ`, `LaurentPolynomial.exists_T_pow`, `MvPolynomial.support_C`, `MvPolynomial.eval₂_comp_right`, `MvPolynomial.map_eval`, `LaurentPolynomial.invert_comp_C`, `LaurentPolynomial.antipode_C_mul_T`, `MvPolynomial.eval₂Hom_smul`, `LaurentPolynomial.degree_C_le`, `char_dvd_card_solutions_of_fintype_sum_lt`, `MvPolynomial.bind₁_monomial`, `LinearMap.polyCharpoly_coeff_eval`, `MvPolynomial.continuous_eval`, `MvPolynomial.C_eq_smul_one`, `MvPolynomial.evalₗ_apply`, `mapDomainRingHom_apply`, `MvPolynomial.map_id`, `MvPolynomial.eval₂Hom_comp_expand`, `Polynomial.toMvPolynomial_C`, `MvPowerSeries.trunc'_C`, `LaurentPolynomial.degree_C_mul_T_le`, `Algebra.Generators.C_mul_X_sub_one_mem_ker`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `MvPowerSeries.trunc'_C_mul`, `MvPolynomial.commAlgEquiv_C_X`, `MvPolynomial.expand_zero_apply`, `WeierstrassCurve.Projective.negDblY_of_Y_eq'`, `mapRingHom_comp_mapDomainRingHom`, `MvPolynomial.eval_polynomial_eval_finSuccEquiv`, `MvPolynomial.constantCoeff_comp_algebraMap`, `MvPolynomial.sumToIter_Xl`, `WittVector.constantCoeff_wittSub`, `MvPolynomial.counit_X`, `MvPolynomial.eval₂Hom_comp_C`
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalNonAssocSemiring` 📖	CompOp	248 math math: `instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums`, `instIsCancelAddZeroOfIsCancelAddOfUniqueSums`, `MonomialOrder.span_leadingTerm_sdiff_singleton_zero`, `mapDomainRingEquiv_apply`, `Polynomial.toLaurent_eq_zero`, `MvPolynomial.coeffs_add`, `Polynomial.ofFinsupp_zero`, `MvPolynomial.zero_divMonomial`, `MonomialOrder.degree_add_of_ne`, `MvPolynomial.mapEquiv_symm`, `MvPolynomial.homogeneousComponent_eq_zero'`, `mapDomainNonUnitalRingHom_id`, `MvPolynomial.instIsReduced`, `MvPolynomial.isEmptyRingEquiv_apply`, `isScalarTower_self`, `MvPolynomial.divMonomial_add_modMonomial`, `MonomialOrder.leadingCoeff_eq_zero_iff`, `MvPolynomial.homogeneousComponent_of_mem`, `mapDomainAddEquiv_single`, `zero_divOf`, `mapDomainNonUnitalAlgHom_apply`, `MvPolynomial.expand_eq_zero`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C`, `Matrix.toMvPolynomial_add`, `MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply`, `mapDomainAddEquiv_apply`, `MvPolynomial.irreducible_mul_X_add`, `WittVector.mul_polyOfInterest_aux2`, `instNoZeroDivisorsOfUniqueSums`, `MvPolynomial.pderiv_one`, `MvPolynomial.pderiv_mul`, `MvPolynomial.eval₂_zero`, `instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums`, `MvPolynomial.aeval_ite_mem_eq_self`, `MvPolynomial.support_sdiff_support_subset_support_add`, `MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt`, `MvPolynomial.monomial_zero`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `MvPolynomial.support_eq_empty`, `uniqueRingEquiv_apply`, `MvPolynomial.mvPolynomialEquivMvPolynomial_apply`, `opRingEquiv_symm_single`, `MonomialOrder.leadingTerm_zero`, `opRingEquiv_symm_apply`, `MonomialOrder.div_single`, `MonomialOrder.image_leadingTerm_sdiff_singleton_zero`, `MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero`, `MonomialOrder.degree_add_le`, `MvPolynomial.weightedHomogeneousComponent_eq_zero'`, `MvPolynomial.IsHomogeneous.add`, `MvPolynomial.coe_eq_zero_iff`, `WeierstrassCurve.Jacobian.polynomialY_eq`, `MvPolynomial.support_add`, `MonomialOrder.sPolynomial_self`, `mapAddEquiv_single`, `supDegree_add_eq_right`, `MvPolynomial.eq_zero_of_eval_eq_zero`, `Polynomial.homogenize_add`, `MonomialOrder.span_leadingTerm_eq_span_monomial₀`, `LinearMap.polyCharpoly_coeff_eq_zero_of_basis`, `MvPolynomial.C_0`, `smulCommClass_symm_self`, `LinearMap.toMvPolynomial_add`, `WeierstrassCurve.Projective.polynomialZ_eq`, `MvPolynomial.coe_zero`, `Polynomial.toFinsupp_eq_zero`, `Polynomial.ofFinsupp_add`, `leadingCoeff_add_eq_right`, `MonomialOrder.monic_X_add_C`, `mapDomainNonUnitalRingHom_apply`, `MvPolynomial.mapEquiv_apply`, `leadingCoeff_eq_zero`, `wittPolynomial_one`, `MvPolynomial.pderiv_X`, `leadingCoeff_add_eq_left`, `MvPolynomial.C_add`, `LinearMap.toMvPolynomial_zero`, `WittVector.mul_polyOfInterest_aux4`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne`, `MvPolynomial.IsWeightedHomogeneous.add`, `MvPolynomial.killCompl_monomial_eq_zero_of_not_subset`, `of'_dvd_iff_modOf_eq_zero`, `MvPolynomial.pderiv_def`, `MvPolynomial.isEmptyRingEquiv_symm_apply`, `Matrix.toMvPolynomial_zero`, `MvPolynomial.modMonomial_add_divMonomial`, `MonomialOrder.span_leadingTerm_eq_span_monomial'`, `MvPolynomial.rename_zero`, `commRingEquiv_single_single`, `mul_of'_modOf`, `MvPolynomial.eq_zero_iff`, `mapAddEquiv_apply`, `MvPowerSeries.truncFinset_monomial_eq_zero`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `algebraicIndependent_iff`, `symm_mapAddEquiv`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none`, `MvPolynomial.eval_add`, `MvPolynomial.isNilpotent_iff`, `MvPolynomial.instNoZeroDivisors`, `MvPolynomial.monomial_eq_zero`, `MonomialOrder.sPolynomial_left_zero`, `MonomialOrder.support_leadingTerm`, `MvPolynomial.eval₂_add`, `MonomialOrder.image_leadingTerm_insert_zero`, `add_divOf`, `mapDomainRingEquiv_trans`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply`, `MvPolynomial.isWeightedHomogeneous_zero`, `MonomialOrder.coeff_degree_eq_zero_iff`, `MonomialOrder.sPolynomial_right_zero`, `WeierstrassCurve.Projective.polynomialX_eq`, `modOf_add_divOf`, `MvPolynomial.totalDegree_add`, `MvPolynomial.coe_add`, `MvPolynomial.modMonomial_X`, `MonomialOrder.leadingCoeff_add_of_lt`, `AlgebraicIndependent.eq_zero_of_aeval_eq_zero`, `WeierstrassCurve.Projective.polynomialY_eq`, `MvPolynomial.weightedHomogeneousComponent_finsupp`, `MvPolynomial.C_eq_zero`, `nonUnitalAlgHom_ext'_iff`, `MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne`, `mapRingEquiv_apply`, `liftMagma_apply_apply`, `MvPolynomial.X_dvd_iff_modMonomial_eq_zero`, `mapDomainNonUnitalRingHom_comp`, `MvPolynomial.homogeneousComponent_eq_zero`, `WeierstrassCurve.Jacobian.polynomialZ_eq`, `opRingEquiv_single`, `liftMagma_symm_apply`, `MvPolynomial.add_divMonomial`, `MvPolynomial.isEmptyRingEquiv_symm_toRingHom`, `MvPolynomial.pderiv_X_of_ne`, `MvPolynomial.IsSymmetric.zero`, `MvPolynomial.degrees_add_le`, `MvPolynomial.isHomogeneous_zero`, `MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt`, `MonomialOrder.span_leadingTerm_insert_zero`, `curryRingEquiv_symm_single`, `opRingEquiv_apply`, `MonomialOrder.div_set`, `mapDomainRingEquiv_single`, `MvPolynomial.X_mul_modMonomial`, `MonomialOrder.degree_zero`, `MvPolynomial.coeff_zero`, `MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem`, `MvPolynomial.totalDegree_zero`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card`, `Polynomial.toFinsuppIso_apply`, `uniqueRingEquiv_symm_apply`, `algebraicIndependent_subtype`, `MonomialOrder.degree_add_eq_right_of_lt`, `symm_mapDomainRingEquiv`, `supDegree_add_eq_left`, `Polynomial.homogenize_monomial_of_lt`, `Polynomial.toFinsupp_add`, `MvPolynomial.weightedHomogeneousComponent_eq_zero`, `MvPolynomial.instIsCancelMulZeroOfIsCancelAdd`, `WittVector.polyOfInterest_vars_eq`, `MvPolynomial.mapEquiv_trans`, `MvPolynomial.pderiv_inr_universalFactorizationMap_X`, `MvPolynomial.degrees_zero`, `divOf_add_modOf`, `MonomialOrder.leadingCoeff_zero`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `MvPolynomial.pderiv_eq_zero_of_notMem_vars`, `MvPolynomial.le_degrees_add_right`, `MvPolynomial.weightedTotalDegree'_zero`, `WeierstrassCurve.Jacobian.polynomialX_eq`, `MvPolynomial.coeff_add`, `MvPolynomial.support_zero`, `MvPolynomial.rename_eq_zero_iff_of_injective`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `WittVector.bind₁_zero_wittPolynomial`, `MvPolynomial.instIsCancelAddOfIsLeftCancelAdd`, `MvPolynomial.degreeOf_zero`, `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero`, `MvPolynomial.divMonomial_add_modMonomial_single`, `mapAddEquiv_trans`, `MvPolynomial.mul_monomial_modMonomial`, `LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis`, `MvPolynomial.mapEquiv_refl`, `MvPolynomial.eval₂_C_mk_eq_zero`, `Polynomial.homogenize_zero`, `MvPolynomial.le_degrees_add_left`, `Polynomial.toFinsuppIso_symm_apply`, `LaurentPolynomial.degree_eq_bot_iff`, `mapDomainAddEquiv_trans`, `MonomialOrder.degree_add_of_lt`, `curryRingEquiv_single`, `MonomialOrder.div`, `MvPolynomial.weightedTotalDegree'_eq_bot_iff`, `MvPolynomial.weightedHomogeneousComponent_of_mem`, `MonomialOrder.degree_X_add_C`, `Polynomial.ofFinsupp_eq_zero`, `MonomialOrder.Monic.add_of_lt`, `addMonoidAlgebraRingEquivDirectSum_apply`, `MvPolynomial.mul_X_modMonomial`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`, `Polynomial.homogenize_eq_zero_iff`, `Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix`, `MvPolynomial.IsSymmetric.add`, `WittVector.mul_polyOfInterest_aux3`, `WittVector.verschiebungPoly_zero`, `MvPolynomial.pderiv_C`, `of'_mul_modOf`, `MvPolynomial.modMonomial_add_divMonomial_single`, `MvPolynomial.C_dvd_iff_zmod`, `WittVector.wittOne_pos_eq_zero`, `algebraicIndependent_comp_subtype`, `MvPolynomial.vars_add_subset`, `MvPolynomial.support_symmDiff_support_subset_support_add`, `LaurentPolynomial.smeval_zero`, `MvPolynomial.isEmptyRingEquiv_eq_coeff_zero`, `of'_modOf`, `symm_mapRingEquiv`, `symm_commRingEquiv`, `MvPolynomial.killCompl_monomial`, `MvPolynomial.degrees_add_of_disjoint`, `symm_mapDomainAddEquiv`, `LaurentPolynomial.smeval_add`, `WittVector.wittZero_eq_zero`, `MvPolynomial.coeff_add_pow`, `Polynomial.toFinsupp_zero`, `MvPolynomial.weightedTotalDegree_zero`, `MvPolynomial.coeffs_zero`, `smulCommClass_self`, `MonomialOrder.leadingTerm_eq_zero_iff`, `MvPolynomial.C_dvd_iff_map_hom_eq_zero`, `MvPolynomial.degreeOf_add_le`, `LaurentPolynomial.degree_zero`, `WittVector.wittAdd_zero`, `MvPolynomial.vars_0`, `MvPolynomial.vars_add_of_disjoint`, `mapRingEquiv_trans`, `MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range`, `MvPolynomial.monomial_modMonomial`, `mapRingEquiv_single`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `Polynomial.coeff_freeMonic`, `MonomialOrder.degree_sPolynomial`, `MvPolynomial.eq_zero_of_eval_zero_at_prod_finset`, `Height.max_mulHeightBound_zero_one_eq_one`, `MvPolynomial.monomial_mul_modMonomial`, `MvPolynomial.pderiv_inl_universalFactorizationMap_X`
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	22 math math: `MvPolynomial.dvd_monomial_one_iff_exists`, `MvPolynomial.exists_dvd_map_of_isAlgebraic`, `MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero`, `MvPolynomial.X_dvd_X`, `MvPolynomial.X_dvd_monomial`, `MvPolynomial.dvd_monomial_iff_exists`, `MvPolynomial.X_dvd_mul_iff`, `of'_dvd_iff_modOf_eq_zero`, `MvPolynomial.dvd_X_mul_iff`, `MvPolynomial.dvd_smul_X_iff_exists`, `MvPolynomial.C_dvd_iff_dvd_coeff`, `MvPolynomial.X_dvd_iff_modMonomial_eq_zero`, `MvPolynomial.dvd_monomial_mul_iff_exists`, `MvPolynomial.dvd_X_iff_exists`, `MvPolynomial.dvd_C_iff_exists`, `MvPolynomial.mem_ideal_span_monomial_image_iff_dvd`, `MvPolynomial.monomial_one_dvd_monomial_one`, `MvPolynomial.C_dvd_iff_zmod`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `MvPolynomial.C_dvd_iff_map_hom_eq_zero`, `Polynomial.homogenize_dvd`, `MvPolynomial.monomial_dvd_monomial`
`of` 📖	CompOp	7 math math: `algHom_ext'_iff`, `of_apply`, `ringHom_ext'_iff`, `lift_of`, `lift_unique'`, `of_injective`, `of'_eq_of`
`of'` 📖	CompOp	23 math math: `of'_mem_span`, `of'_divOf`, `of'_commute`, `of'_mul_divOf`, `mvPolynomial_aeval_of_surjective_of_closure`, `mem_ideal_span_of'_image`, `of'_dvd_iff_modOf_eq_zero`, `mul_of'_modOf`, `modOf_add_divOf`, `exists_finset_adjoin_eq_top`, `of'_apply`, `lift_of'`, `mem_adjoin_support`, `divOf_add_modOf`, `support_gen_of_gen`, `mem_span_support'`, `of'_mul_modOf`, `of'_modOf`, `support_gen_of_gen'`, `of'_eq_of`, `mem_span_support`, `freeAlgebra_lift_of_surjective_of_closure`, `mul_of'_divOf`
`ofCoeff` 📖	CompOp	21 math math: `coeffEquiv_symm_apply`, `ofCoeff_update`, `exists`, `ofCoeff_eq_zero`, `supportedEquivFinsupp_apply_support_val`, `ofCoeff_neg`, `ofCoeff_coeff`, `ofCoeff_injective`, `ofCoeff_erase`, `ofCoeff_sub`, `forall`, `ofCoeff_mapRange`, `ofCoeff_zero`, `coeffAddEquiv_symm_apply`, `ofCoeff_add`, `coeffLinearEquiv_symm_apply`, `ofCoeff_inj`, `ofCoeff_sum`, `coeff_ofCoeff`, `ofCoeff_finsuppSum`, `ofCoeff_smul`
`ofMagma` 📖	CompOp	3 math math: `nonUnitalAlgHom_ext'_iff`, `ofMagma_apply`, `liftMagma_symm_apply`
`semiring` 📖	CompOp	905 math math: `MvPolynomial.pUnitAlgEquiv_symm_monomial`, `MvPolynomial.join₁_rename`, `MvPolynomial.vanishingIdeal_anti_mono`, `MvPolynomial.aeval_sum`, `mapRangeAlgEquiv_trans`, `WittVector.bind₁_frobeniusPoly_wittPolynomial`, `KaehlerDifferential.mvPolynomialBasis_apply`, `Algebra.PreSubmersivePresentation.jacobiMatrix_naive`, `lift_apply'`, `MvPolynomial.algHom_ext_iff`, `MonomialOrder.span_leadingTerm_sdiff_singleton_zero`, `MvPolynomial.map_bind₁`, `Algebra.Generators.aeval_val_surjective`, `domCongr_comp_lsingle`, `wittPolynomial_zmod_self`, `MvPolynomial.aeval_X_left`, `MvPolynomial.pUnitAlgEquiv_apply`, `algHom_ext'_iff`, `MvPolynomial.exists_finset_rename`, `MvPolynomial.support_finSuccEquiv`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_apply`, `WittVector.aeval_verschiebung_poly'`, `MvPolynomial.rTensorAlgEquiv_apply`, `Algebra.Generators.H1Cotangent.δAux_mul`, `Algebra.Presentation.naive_toGenerators`, `MvPolynomial.mem_image_support_coeff_finSuccEquiv`, `MvPolynomial.comapEquiv_symm_coe`, `Matrix.charpoly.univ_map_map`, `MvPolynomial.eval₂_expand`, `MvPolynomial.universalFactorizationMap_comp_map`, `MvPolynomial.aeval_algebraMap_eq_zero_iff`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_map`, `MvPolynomial.expand_X`, `algebraicIndependent_iff_ker_eq_bot`, `Algebra.Generators.cotangentSpaceBasis_apply`, `MvPolynomial.instIsReduced`, `MvPolynomial.X_pow_eq_monomial`, `WittVector.ghostComponent_apply`, `MvPolynomial.ker_map`, `aeval_wittPolynomial`, `MvPolynomial.aeval_range`, `KaehlerDifferential.mvPolynomialBasis_repr_D_X`, `MvPolynomial.optionEquivLeft_C`, `MvPolynomial.rename_rename`, `Algebra.Generators.toAlgHom_ofComp_localizationAway`, `MvPolynomial.leibniz_iff_X`, `MvPowerSeries.trunc'_expand_trunc'`, `MvPolynomial.optionEquivLeft_X_some`, `Polynomial.toFinsupp_pow`, `MvPolynomial.aeval_X_left_apply`, `Polynomial.toPowerSeries_toMvPowerSeries`, `MvPolynomial.le_vanishingIdeal_zeroLocus`, `MvPolynomial.pUnitAlgEquiv_symm_apply`, `MvPolynomial.expand_eq_zero`, `MvPolynomial.weightedHomogeneousSubmodule_mul`, `Ideal.span_pow_eq_map_homogeneousSubmodule`, `MvPolynomial.natDegree_finSuccEquiv`, `StandardEtalePresentation.toPresentation_algebra_smul`, `MvPolynomial.totalDegree_X_pow`, `Ideal.span_eq_map_homogeneousSubmodule`, `domCongr_toAlgHom`, `MvPolynomial.algHom_ext'_iff`, `IntermediateField.mem_adjoin_iff`, `AlgebraicIndependent.repr_ker`, `chevalley_mvPolynomial_mvPolynomial`, `MvPolynomial.aeval_X`, `MvPolynomial.comapEquiv_coe`, `Polynomial.pUnitAlgEquiv_symm_toPowerSeries`, `MvPolynomial.eval₂_pow`, `MvPolynomial.irreducible_mul_X_add`, `AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin`, `Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff`, `MvPolynomial.optionEquivLeft_apply`, `MvPolynomial.instIsScalarTower`, `MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le`, `MvPolynomial.map_comp_rename`, `MvPolynomial.ACounit_X`, `WittVector.mul_polyOfInterest_aux2`, `MvPolynomial.prime_rename_iff`, `bind₁_xInTermsOfW_wittPolynomial`, `MvPolynomial.constantCoeff_rename`, `Algebra.PreSubmersivePresentation.jacobiMatrix_reindex`, `AlgebraicClosure.maxIdeal.isMaximal`, `CommRingCat.free_map_coe`, `Algebra.FinitePresentation.mvPolynomial_of_finitePresentation`, `Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap`, `MvPolynomial.killCompl_comp_rename`, `MvPolynomial.supportedEquivMvPolynomial_symm_X`, `Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp`, `MvPolynomial.ACounit_surjective`, `lift_mapRangeRingHom_algebraMap`, `MvPolynomial.supported_eq_adjoin_X`, `MvPolynomial.aeval_eq_eval`, `mapAlgHom_single`, `MvPolynomial.aeval_ite_mem_eq_self`, `MvPolynomial.eval₂Hom_C_id_eq_join₁`, `LaurentPolynomial.T_pow`, `PolynomialLaw.exists_lift'`, `MvPolynomial.pow_idealOfVars`, `PolynomialLaw.toFun_eq_rTensor_φ_toFun'`, `MvPolynomial.comap_id`, `MvPolynomial.eval_rename_prod_mk`, `MvPolynomial.optionEquivRight_C`, `mapDomainBialgHom_id`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `MvPolynomial.aevalTower_comp_C`, `MvPolynomial.rename_msymm`, `MvPolynomial.comap_comp_apply`, `MvPolynomial.eval₂Hom_C_eq_bind₁`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_relation`, `MvPolynomial.degreeOf_coeff_finSuccEquiv`, `mapDomainAlgHom_id`, `MvPolynomial.mem_pow_idealOfVars_iff`, `MvPolynomial.rename_id_apply`, `toRingHom_mapAlgHom`, `MvPolynomial.nonempty_support_finSuccEquiv`, `Algebra.Generators.cotangentSpaceBasis_repr_one_tmul`, `MvPolynomial.pderiv_rename`, `Algebra.Presentation.comp_relation_inr`, `LinearMap.nilRankAux_basis_indep`, `MvPolynomial.support_killCompl`, `AlgebraicIndependent.aeval_comp_repr`, `MvPolynomial.esymmAlgHomMonomial_single`, `MvPolynomial.map_expand`, `MvPolynomial.map_aeval`, `MvPolynomial.map_frobenius_expand`, `MvPolynomial.renameEquiv_trans`, `MvPolynomial.expand_monomial`, `algebraMap_def`, `MvPolynomial.expand_char`, `MvPolynomial.map_rename`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_σ'`, `MvPolynomial.killCompl_C`, `LaurentPolynomial.algebraMap_apply`, `MvPolynomial.eval₂_const_pUnitAlgEquiv_symm`, `MvPolynomial.eval_comp_toMvPolynomial`, `Algebra.Generators.map_toComp_ker`, `MvPolynomial.support_finSuccEquiv_nonempty`, `Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply`, `MvPolynomial.bind₁_X_left`, `MvPolynomial.sumAlgEquiv_comp_rename_inr`, `MvPolynomial.aevalTower_toAlgHom`, `LinearMap.polyCharpoly_coeff_isHomogeneous`, `MvPolynomial.degree_optionEquivLeft`, `MvPolynomial.mapAlgHom_id`, `Algebra.Generators.naive_val`, `MvPolynomial.coeff_expand_smul`, `LaurentPolynomial.antipode_T`, `Algebra.Generators.algebraMap_apply`, `mapDomainRingHom_comp_algebraMap`, `MvPolynomial.expand_C`, `Monic.pow`, `Algebra.Generators.compLocalizationAwayAlgHom_X_inl`, `MvPolynomial.optionEquivRight_X_none`, `MvPolynomial.rename_psum`, `Algebra.Generators.map_ofComp_ker`, `mapDomainBialgHom_mapDomainBialgHom`, `BoundedContinuousFunction.charAlgHom_apply`, `WeierstrassCurve.Jacobian.polynomialY_eq`, `MvPolynomial.expand_zero`, `MvPolynomial.degreesLE_nsmul`, `MvPolynomial.totalDegree_rename_le`, `domCongr_refl`, `MvPolynomial.coe_mapEquivMonic_comp'`, `Algebra.Presentation.naive_relation`, `decomposeAux_coe`, `Polynomial.toMvPolynomial_eq_rename_comp`, `DividedPowerAlgebra.dp_mul`, `Polynomial.ofFinsupp_pow`, `Polynomial.aeval_homogenize_X_one`, `MvPolynomial.adjoin_range_X`, `MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure`, `mvPolynomial_aeval_of_surjective_of_closure`, `MvPolynomial.transcendental_polynomial_aeval_X_iff`, `MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective`, `Algebra.Generators.algebraMap_eq`, `Algebra.SubmersivePresentation.ofSubsingleton_relation`, `StandardEtalePair.equivMvPolynomialQuotient_symm_apply`, `MvPolynomial.support_rename_of_injective`, `Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial`, `MvPolynomial.comap_comp`, `xInTermsOfW_eq`, `LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree`, `MvPolynomial.eval_eq_eval_mv_eval'`, `MvPolynomial.ACounit_C`, `LinearMap.polyCharpoly_baseChange`, `MvPolynomial.transcendental_supported_X_iff`, `MvPolynomial.optionEquivLeft_X_none`, `MvPolynomial.algebraicIndependent_polynomial_aeval_X`, `MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring`, `MvPolynomial.degreeOf_rename_of_injective`, `MvPolynomial.degreesLE_add`, `mapRingHom_comp_algebraMap`, `MvPolynomial.exists_rename_eq_of_vars_subset_range`, `MonomialOrder.span_leadingTerm_eq_span_monomial`, `MvPolynomial.optionEquivRight_symm_apply`, `MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet`, `MonomialOrder.span_leadingTerm_eq_span_monomial₀`, `tensorEquiv.invFun_tmul`, `LinearMap.polyCharpolyAux_map_eval`, `LinearMap.polyCharpoly_coeff_eq_zero_of_basis`, `Algebra.Generators.Hom.aeval_val`, `Polynomial.MonicDegreeEq.freeMonic_coe`, `Polynomial.ofFinsupp_algebraMap`, `DividedPowerAlgebra.natFactorial_mul_dp_eq`, `Algebra.Presentation.comp_aeval_relation_inl`, `WittVector.mulN_coeff`, `MvPolynomial.isUnit_iff_totalDegree_of_isReduced`, `isLocalHom_singleZeroRingHom`, `MvPolynomial.support_expand_subset`, `commAlgEquiv_single_single`, `WeierstrassCurve.Projective.polynomialZ_eq`, `Matrix.charpoly.univ_monic`, `MvPolynomial.totalDegree_pow`, `MvPolynomial.coeff_rename_embDomain`, `MvPolynomial.isUnit_iff`, `MvPolynomial.finSuccEquiv_coeff_coeff`, `MvPolynomial.rename_comp_expand`, `Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'`, `MvPolynomial.rename_esymm`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply`, `MvPolynomial.quotient_map_C_eq_zero`, `MvPolynomial.coeff_X_pow`, `isLocalHom_algebraMap`, `lift_apply`, `MvPolynomial.pow_idealOfVars_eq_span`, `mem_ideal_span_of'_image`, `MvPolynomial.IsHomogeneous.pow`, `Algebra.Generators.toAlgHom_ofComp_surjective`, `MvPolynomial.bind₁_comp_bind₁`, `MvPolynomial.commAlgEquiv_C`, `Algebra.Generators.Hom.algebraMap_toAlgHom'`, `Algebra.FinitePresentation.ker_fg_of_mvPolynomial`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `MvPolynomial.aevalTower_X`, `MvPolynomial.irreducible_of_forall_totalDegree_le`, `MvPolynomial.commAlgEquiv_X`, `Matrix.charpoly.univ_coeff_eval₂Hom`, `MvPolynomial.optionEquivRight_X_some`, `MvPolynomial.aeval_expand`, `AlgebraicIndependent.lift_reprField`, `domCongr_single`, `MvPolynomial.aeval_algebraMap_apply`, `Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation`, `wittPolynomial_one`, `Algebra.FiniteType.baseChangeAux_surj`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `Subalgebra.mvPolynomial_aeval_coe`, `IsLocalization.Away.mvPolynomialQuotientEquiv_apply`, `mapDomainBialgHom_apply`, `coe_algebraMap`, `Algebra.Presentation.naive_relation_apply`, `le_inf_support_pow`, `PolynomialLaw.exists_lift`, `WittVector.mul_polyOfInterest_aux4`, `MvPolynomial.rename_eval₂`, `MvPolynomial.coeff_sum_X_pow_of_fintype`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `MvPowerSeries.expand_eq_expand`, `MvPolynomial.irreducible_of_disjoint_support`, `Algebra.Generators.localizationAway_σ`, `MvPolynomial.mapAlgEquiv_apply`, `Polynomial.Bivariate.equivMvPolynomial_symm_X_0`, `MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval`, `MvPolynomial.finitePresentation_universalFactorizationMap`, `MvPolynomial.mapAlgEquiv_refl`, `WittVector.frobeniusPoly_zmod`, `Algebra.FiniteType.iff_quotient_mvPolynomial'`, `MvPolynomial.tensorEquivSum_one_tmul_C`, `MonomialOrder.Monic.pow`, `Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom`, `Polynomial.degree_freeMonic`, `MvPolynomial.eval₂Hom_rename`, `MvPolynomial.degreeOf_pow_eq`, `LieModule.rank_eq_natTrailingDegree`, `MvPolynomial.sumAlgEquiv_comp_rename_inl`, `AlgebraicIndependent.aeval_of_algebraicIndependent`, `MvPolynomial.aeval_bind₁`, `MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero`, `MvPolynomial.algebraMap_apply`, `MvPolynomial.mkDerivationₗ_monomial`, `MvPolynomial.killCompl_monomial_eq_zero_of_not_subset`, `MvPolynomial.exists_fin_rename`, `MvPolynomial.optionEquivLeft_coeff_coeff`, `Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous`, `MvPolynomial.pderiv_def`, `MvPolynomial.mem_pow_idealOfVars_iff'`, `MvPolynomial.mem_supported`, `MvPolynomial.renameEquiv_apply`, `MvPolynomial.degrees_pow_le`, `MvPolynomial.rename_esymmAlgHom`, `finiteType_of_fg`, `MvPolynomial.aeval_eq_zero`, `MvPolynomial.eval₂_cast_comp`, `Algebra.PreSubmersivePresentation.naive_toPresentation`, `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `MonomialOrder.span_leadingTerm_eq_span_monomial'`, `MvPolynomial.bind₁_C_right`, `Polynomial.toTupleMvPolynomial_one_eq`, `MvPolynomial.rename_zero`, `MvPolynomial.instIsLocalHomRingHomAlgebraMap`, `WittVector.bind₁_wittMulN_wittPolynomial`, `PolynomialLaw.exists_range_φ_eq_of_fg`, `Algebra.FinitePresentation.mvPolynomial`, `MvPolynomial.coeff_single_X_pow`, `commRingEquiv_single_single`, `MvPolynomial.aevalTower_C`, `MvPolynomial.expand_one_apply`, `MvPolynomial.map_expand_pow_char`, `xInTermsOfW_aux`, `Algebra.Presentation.span_range_relation_eq_ker`, `MvPolynomial.monomial_mem_pow_idealOfVars_iff`, `MonomialOrder.degree_smul_le`, `MvPolynomial.irreducible_sumSMulX`, `AnalyticOnNhd.aeval_mvPolynomial`, `Algebra.Generators.Hom.toAlgHom_X`, `MvPolynomial.bind₁_rename`, `wittStructureRat_prop`, `MvPolynomial.degrees_rename`, `Algebra.Presentation.comp_relation`, `Polynomial.Bivariate.equivMvPolynomial_symm_C`, `Algebra.Generators.instIsScalarTowerRing`, `MvPowerSeries.aeval_coe`, `LaurentPolynomial.algebraMap_X_pow`, `Polynomial.homogenize_X_pow`, `WittVector.IsPoly.poly`, `finiteType_iff_group_fg`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `MvPolynomial.finite_universalFactorizationMap`, `MvPolynomial.rTensorAlgHom_toLinearMap`, `wittStructureRat_rec`, `WittVector.mul_polyOfInterest_vars`, `MvPolynomial.homogeneousSubmodule_zero`, `MvPolynomial.expand_eq_C`, `MvPowerSeries.trunc'_expand`, `MvPolynomial.universalFactorizationMapPresentation_map`, `MvPolynomial.coeff_rename_mapDomain`, `MvPolynomial.algebraTensorAlgEquiv_symm_X`, `MvPolynomial.expand_injective`, `MvPolynomial.support_coeff_finSuccEquiv`, `Algebra.Presentation.aeval_val_relation`, `LinearMap.polyCharpolyAux_map_eq_charpoly`, `MvPolynomial.expand_one`, `MvPolynomial.esymmAlgHom_fin_surjective`, `MvPolynomial.expand_inj`, `LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff`, `MvPolynomial.coeff_prod_X_pow`, `MvPolynomial.coeffsIn_mul`, `MvPowerSeries.rename_coe`, `MvPolynomial.mk_eq_eval₂`, `Algebra.Generators.H1Cotangent.δAux_ofComp`, `MvPolynomial.restrictSupport_zero`, `LaurentPolynomial.algebraMap_eq_toLaurent`, `MvPolynomial.killCompl_monomial_mapDomain`, `MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors`, `MvPolynomial.isUnit_iff_eq_C_of_isReduced`, `MvPolynomial.monomial_add_single`, `MvPolynomial.le_coeffsIn_pow`, `MvPolynomial.supported_strictMono`, `MvPolynomial.IsWeightedHomogeneous.pow`, `MonomialOrder.degree_pow_le`, `MvPolynomial.pointToPoint_zeroLocus_le`, `exists_integral_inj_algHom_of_quotient`, `MvPolynomial.isNilpotent_iff`, `exists_finite_inj_algHom_of_fg`, `toDirectSum_pow`, `MvPolynomial.zeroLocus_bot`, `MvPolynomial.aeval_def`, `lift_single`, `Algebra.Generators.toAlgHom_ofComp_rename`, `mapDomainAlgHom_apply`, `Algebra.FinitePresentation.iff`, `DividedPowerAlgebra.dp_zero`, `wittStructureRat_rec_aux`, `Polynomial.Bivariate.equivMvPolynomial_symm_X_1`, `MvPolynomial.supported_mono`, `Algebra.Generators.ker_localizationAway`, `MonomialOrder.sPolynomial_decomposition`, `MvPolynomial.totalDegree_expand`, `MvPolynomial.algHom_C`, `lift_symm_apply`, `wittStructureInt_prop`, `MvPolynomial.eval_pow`, `AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply`, `MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal`, `MvPolynomial.mem_support_coeff_optionEquivLeft`, `Algebra.Presentation.fg_ker`, `Polynomial.eval_X_toTupleMvPolynomial_zero_eq`, `MvPolynomial.dvd_smul_X_iff_exists`, `MvPolynomial.mem_supported_vars`, `MvPolynomial.mkDerivation_monomial`, `LaurentPolynomial.isUnit_T`, `Algebra.Presentation.relation_mem_ker`, `Algebra.Generators.Hom.toExtensionHom_toRingHom`, `Algebra.Generators.comp_localizationAway_ker`, `MvPolynomial.mem_map_C_iff`, `MvPolynomial.rename_monomial`, `MvPolynomial.aeval_toMvPolynomial`, `MvPolynomial.mul_esymm_eq_sum`, `MvPolynomial.restrictScalars_restrictSupportIdeal`, `MvPolynomial.degreesLE_zero`, `GradesBy.decompose_single`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `MvPolynomial.aevalTower_comp_algebraMap`, `Algebra.PreSubmersivePresentation.aevalDifferential_single`, `AlgebraicIndependent.algebraMap_aevalEquiv`, `MvPolynomial.aeval_id_rename`, `mapAlgHom_apply`, `WeierstrassCurve.Projective.polynomialX_eq`, `Algebra.adjoin_range_eq_range_aeval`, `coe_liftNCAlgHom`, `Algebra.Generators.aeval_val_σ`, `MvPolynomial.mem_zeroLocus_iff`, `MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le`, `WeierstrassCurve.Projective.polynomialY_eq`, `MvPolynomial.aeval_eq_constantCoeff_of_vars`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul`, `lift_of`, `SymmetricAlgebra.equivMvPolynomial_symm_X`, `MvPolynomial.coeff_linearCombination_X_pow`, `MvPolynomial.expand_bind₁`, `MvPolynomial.prod_X_pow_eq_monomial`, `MvPolynomial.smul_eval`, `MvPowerSeries.substAlgHom_coe`, `MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap`, `MvPolynomial.coeff_rTensorAlgHom_tmul`, `MvPolynomial.aeval_zero`, `MvPolynomial.killCompl_rename_app`, `MvPolynomial.comp_aeval`, `MvPolynomial.frobenius_zmod`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `WittVector.frobeniusPolyAux_eq`, `MvPolynomial.optionEquivLeft_coeff_some_coeff_none`, `IntermediateField.mem_adjoin_range_iff`, `DividedPowerAlgebra.mkAlgHom_surjective`, `WittVector.coeff_frobeniusFun`, `MvPolynomial.renameEquiv_refl`, `MvPolynomial.totalDegree_renameEquiv`, `MvPolynomial.expand_mul`, `LaurentPolynomial.C_eq_algebraMap`, `Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul`, `MvPolynomial.isLocalHom_expand`, `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `MvPolynomial.C_mul'`, `AlgebraicClosure.le_maxIdeal`, `MvPolynomial.isEmptyAlgEquiv_apply`, `MvPolynomial.of_irreducible_expand`, `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`, `LinearMap.polyCharpolyAux_baseChange`, `Polynomial.Bivariate.equivMvPolynomial_X`, `Module.Basis.symmetricAlgebra_repr_apply`, `MonomialOrder.degree_smul_of_isRegular`, `AlgebraicClosure.toSplittingField_coeff`, `MvPolynomial.coe_pow`, `MvPolynomial.natDegree_optionEquivLeft`, `Matrix.charpoly.univ_coeff_isHomogeneous`, `mapDomain_algebraMap`, `Algebra.Generators.self_algebra_smul`, `exists_finset_adjoin_eq_top`, `MvPolynomial.restrictSupport_nsmul`, `MvPolynomial.mem_support_finSuccEquiv`, `MvPolynomial.isNoetherianRing_fin`, `algebraicIndependent_iff_injective_aeval`, `MvPolynomial.aeval_map_algebraMap`, `Algebra.Generators.Hom.toAlgHom_C`, `MvPolynomial.rename_comp_toMvPolynomial`, `MvPolynomial.finSuccEquiv_comp_C_eq_C`, `MvPolynomial.coeToMvPowerSeries.algHom_apply`, `AlgebraicIndependent.liftAlgHom_comp_reprField`, `DividedPowerAlgebra.algHom_ext_iff`, `MvPolynomial.rename_rightInverse`, `WeierstrassCurve.Jacobian.polynomialZ_eq`, `MvPolynomial.finSuccEquiv_eq`, `SymmetricAlgebra.equivMvPolynomial_ι_apply`, `lift_unique'`, `LinearMap.polyCharpoly_eq_of_basis`, `MvPolynomial.ker_eval₂Hom_universalFactorizationMap`, `MvPolynomial.bind₁_comp_rename`, `LinearMap.polyCharpolyAux_map_aeval`, `MvPolynomial.monic_monomial_eq`, `MvPolynomial.image_support_finSuccEquiv`, `MvPolynomial.eval₂_rename`, `AlgebraicIndependent.aeval_repr`, `MvPolynomial.support_expand`, `tensorEquiv_tmul`, `gradeBy.gradedMonoid`, `Polynomial.toFinsupp_algebraMap`, `LaurentPolynomial.invert_symm`, `Polynomial.Bivariate.equivMvPolynomial_C_X`, `MvPolynomial.IsSymmetric.rename`, `MvPolynomial.IsHomogeneous.aeval`, `WittVector.mul_polyOfInterest_aux1`, `MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse`, `symm_commAlgEquiv`, `MvPolynomial.aeval_bind₂`, `MvPolynomial.rename_bind₁`, `MvPolynomial.support_X_pow`, `MvPolynomial.prod_X_add_C_coeff`, `MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe`, `Algebra.Generators.Hom.toAlgHom_comp_apply`, `MvPolynomial.degree_finSuccEquiv`, `Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial`, `MvPolynomial.isNoetherianRing_fin_0`, `MvPolynomial.nonempty_support_optionEquivLeft`, `MvPolynomial.isRegular_X_pow`, `bind₁_rename_expand_wittPolynomial`, `Algebra.adjoin_eq_range`, `MvPolynomial.mapAlgEquiv_symm`, `Algebra.Generators.toComp_toAlgHom_monomial`, `MvPolynomial.rename_injective`, `MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree`, `Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs`, `mapDomainAlgHom_comp`, `LinearMap.polyCharpolyAux_coeff_eval`, `MvPolynomial.esymmAlgHomMonomial_single_one`, `tensorEquiv_symm_single`, `AlgebraicClosure.Monics.map_eq_prod`, `lift_of'`, `MvPolynomial.coe_smul`, `MvPolynomial.killCompl_map`, `MonomialOrder.span_leadingTerm_insert_zero`, `Algebra.FiniteType.iff_quotient_mvPolynomial`, `curryRingEquiv_symm_single`, `MonomialOrder.div_set`, `grade.decompose_single`, `MvPolynomial.support_optionEquivLeft`, `MvPolynomial.degreeOf_pow_le`, `MvPolynomial.dvd_X_iff_exists`, `MvPolynomial.finSuccEquiv_X_succ`, `MvPolynomial.aeval_ofNat`, `mem_adjoin_support`, `Algebra.Presentation.aeval_val_relationOfHasCoeffs`, `MvPolynomial.expand_comp_bind₁`, `MvPolynomial.mapAlgEquiv_trans`, `Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs`, `MvPolynomial.ker_mapAlgHom`, `MvPolynomial.aeval_injective_iff_of_isEmpty`, `Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp`, `Algebra.Generators.ofComp_kerCompPreimage`, `MvPolynomial.X_mem_supported`, `MvPolynomial.esymmAlgHom_fin_injective`, `MvPolynomial.aeval_comp_bind₁`, `domCongr_support`, `Polynomial.monic_freeMonic`, `MvPolynomial.eval₂_const_pUnitAlgEquiv`, `Algebra.Generators.repr_CotangentSpaceMap`, `DividedPowerAlgebra.dp_sum_smul`, `MvPolynomial.pderiv_pow`, `MvPolynomial.aeval_esymm_eq_multiset_esymm`, `MvPolynomial.supported_le_supported_iff`, `MonomialOrder.coeff_pow_nsmul_degree`, `MvPolynomial.eval_rename`, `StandardEtalePresentation.toPresentation_σ'`, `witt_structure_prop`, `Monic.supDegree_pow`, `MvPolynomial.coe_eval₂AlgHom`, `LinearMap.toMvPolynomial_comp`, `MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff`, `MvPolynomial.vars_bind₁`, `MonomialOrder.leadingCoeff_pow`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `MvPolynomial.prod_C_add_X_eq_sum_esymm`, `Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite`, `lift_mapRingHom_algebraMap`, `MonomialOrder.degree_pow`, `MvPolynomial.optionEquivRight_apply`, `MvPolynomial.finSuccEquiv_apply`, `MvPolynomial.vanishingIdeal_empty`, `MvPolynomial.tensorEquivSum_X_tmul_X`, `curryAlgEquiv_symm_single`, `domCongr_symm`, `MvPolynomial.comp_aeval_apply`, `Algebra.Presentation.relation_comp_localizationAway_inl`, `WittVector.coeff_select`, `MvPolynomial.aeval_unique`, `DividedPowerAlgebra.dp_def`, `MvPolynomial.coeff_rTensorAlgHom_monomial_tmul`, `MvPolynomial.bind₁_bind₁`, `MvPolynomial.algebraTensorAlgEquiv_symm_map`, `MvPolynomial.rename_polynomial_aeval_X`, `MvPolynomial.coeff_expand_of_not_dvd`, `DividedPowerAlgebra.dp_sum`, `Algebra.Generators.Hom.equivAlgHom_symm_apply_val`, `MvPolynomial.isHomogeneous_C_mul_X_pow`, `MvPolynomial.tensorEquivSum_C_tmul_one`, `MvPolynomial.map_iterateFrobenius_expand`, `MvPolynomial.vars_pow`, `Polynomial.toMvPolynomial_X`, `MvPolynomial.sumAlgEquiv_apply`, `algHom_ext_iff`, `Algebra.Generators.ker_comp_eq_sup`, `LinearMap.polyCharpoly_map_eq_charpoly`, `sup_support_pow_le`, `LinearMap.polyCharpoly_monic`, `Polynomial.natDegree_freeMonic`, `Algebra.Generators.ofComp_toAlgHom_monomial_sumElim`, `MvPolynomial.exists_finset_rename₂`, `LaurentPolynomial.invert_apply`, `Matrix.charpoly.univ_natDegree`, `MvPolynomial.algebraMap_eq`, `MvPolynomial.eval_toMvPolynomial`, `Algebra.Presentation.algebraTensorAlgEquiv_symm_relation`, `Algebra.Generators.aeval_val_eq_zero`, `MvPolynomial.coeffsIn_pow`, `MvPolynomial.esymmAlgHom_apply`, `MvPolynomial.monomial_eq`, `BoundedContinuousFunction.star_mem_range_charAlgHom`, `MvPolynomial.aeval_eq_eval₂Hom`, `MvPolynomial.rename_prod_mk_eval₂`, `AlgebraicIndependent.aevalEquivField_apply_coe`, `MvPolynomial.IsSymmetric.smul`, `MvPolynomial.aeval_C`, `MvPolynomial.toMvPowerSeries_pUnitAlgEquiv`, `MvPolynomial.transcendental_polynomial_aeval_X`, `MvPolynomial.aeval_comp_expand`, `Algebra.Generators.naive_σ`, `AlgebraicIndependent.aevalEquiv_apply_coe`, `MvPolynomial.rename_C`, `MvPolynomial.HomogeneousSubmodule.gradedMonoid`, `StandardEtalePresentation.aeval_val_equivMvPolynomial`, `MvPolynomial.aevalTower_comp_toAlgHom`, `MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection`, `MvPolynomial.restrictSupport_add`, `MvPolynomial.eval₂_X_pow`, `MvPolynomial.zeroLocus_span`, `MvPolynomial.IsHomogeneous.rename_isHomogeneous`, `WittVector.polyOfInterest_vars_eq`, `MvPolynomial.isNoetherianRing`, `MvPolynomial.pderiv_inr_universalFactorizationMap_X`, `MvPolynomial.sumAlgEquiv_symm_apply`, `MvPolynomial.eval₂_pUnitAlgEquiv_symm`, `Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul`, `Algebra.Generators.ker_eq_ker_aeval_val`, `mapDomainBialgHom_comp`, `LaurentPolynomial.antipode_C`, `Algebra.Generators.ker_ofAlgHom`, `scalarTensorEquiv_symm_single`, `MvPolynomial.supported_empty`, `MvPolynomial.C_mem_pow_idealOfVars_iff`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `WeierstrassCurve.Jacobian.polynomialX_eq`, `MvPolynomial.aeval_C_comp_left`, `MvPolynomial.C_mul_X_pow_eq_monomial`, `MvPolynomial.degrees_rename_of_injective`, `PolynomialLaw.range_φ`, `MvPolynomial.psum_eq_mul_esymm_sub_sum`, `Polynomial.toFinsuppIsoAlg_apply`, `finiteType_iff_fg`, `MvPolynomial.mapAlgHom_apply`, `Algebra.Generators.cotangentRestrict_mk`, `MvPolynomial.optionEquivLeft_monomial`, `MvPolynomial.rename_eq_zero_iff_of_injective`, `Algebra.Generators.H1Cotangent.δ_eq_δAux`, `Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `LieAlgebra.rank_eq_natTrailingDegree`, `WittVector.bind₁_onePoly_wittPolynomial`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `MvPolynomial.optionEquivLeft_symm_apply`, `MvPolynomial.algebraTensorAlgEquiv_tmul`, `MvPolynomial.mem_support_coeff_finSuccEquiv`, `Algebra.Generators.aeval_val_σ'`, `Algebra.Generators.Hom.toAlgHom_id`, `Algebra.Generators.Hom.comp_val`, `single_pow`, `MvPolynomial.comap_apply`, `MvPolynomial.vars_rename`, `WittVector.bind₁_zero_wittPolynomial`, `StandardEtalePresentation.toPresentation_val`, `MvPolynomial.rename_comp_bind₁`, `MvPolynomial.zeroLocus_top`, `MvPolynomial.rename_X`, `MvPolynomial.pUnitAlgEquiv_monomial`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `MvPolynomial.mem_ideal_span_monomial_image_iff_dvd`, `Matrix.charpoly.univ_map_eval₂Hom`, `MvPolynomial.comap_id_apply`, `MvPolynomial.aeval_one_tmul`, `MvPolynomial.monomial_pow`, `domCongr_apply`, `MvPolynomial.smul_eq_C_mul`, `MvPolynomial.finSuccEquiv_rename_finSuccEquiv`, `MvPolynomial.rename_expand`, `MvPolynomial.homogeneousSubmodule_one_pow`, `Algebra.Generators.fg_ker_of_finitePresentation`, `MvPolynomial.prod_X_pow`, `MvPolynomial.universalFactorizationMapPresentation_algebra_smul`, `MonomialOrder.degree_smul`, `Algebra.FiniteType.instMvPolynomialOfFinite`, `MvPolynomial.derivation_C_mul`, `MvPolynomial.aeval_sumElim_pderiv_inl`, `AnalyticAt.aeval_mvPolynomial`, `MvPolynomial.tensorEquivSum_one_tmul_X`, `LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis`, `support_gen_of_gen`, `MvPolynomial.supported_univ`, `MvPolynomial.isSymmetric_rename`, `MvPolynomial.universalFactorizationMap_freeMonic`, `Algebra.Generators.Hom.toAlgHom_monomial`, `MonomialOrder.sPolynomial_mem_ideal`, `MvPolynomial.mem_ideal_of_coeff_mem_ideal`, `MvPolynomial.irreducible_of_totalDegree_eq_one`, `MvPolynomial.universalFactorizationMapPresentation_val`, `MvPolynomial.rename_comp_rename`, `MvPolynomial.coe_expand`, `MvPolynomial.aeval_sumElim`, `MvPolynomial.universalFactorizationMapPresentation_σ'`, `MvPolynomial.aeval_comp_rename`, `KaehlerDifferential.mvPolynomialBasis_repr_symm_single`, `MvPolynomial.mem_symmetricSubalgebra`, `decomposeAux_single`, `MvPolynomial.support_rename_killCompl_subset`, `MvPolynomial.eval₂_rename_prod_mk`, `AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `MvPolynomial.coeff_linearCombination_X_pow_of_fintype`, `MvPolynomial.mapAlgHom_coe_ringHom`, `bind₁_wittPolynomial_xInTermsOfW`, `Algebra.FinitePresentation.out`, `MvPolynomial.rename_leftInverse`, `Algebra.FiniteType.iff_quotient_mvPolynomial''`, `MvPolynomial.esymmAlgHom_fin_bijective`, `MvPolynomial.esymmAlgEquiv_apply`, `Polynomial.homogenize_C`, `MvPolynomial.eval₂AlgHom_X`, `MvPolynomial.mem_vanishingIdeal_iff`, `MvPolynomial.mem_vanishingIdeal_singleton_iff`, `curryRingEquiv_single`, `MonomialOrder.div`, `WittVector.mul_polyOfInterest_aux5`, `MvPolynomial.expand_zmod`, `MvPolynomial.aeval_zero'`, `MvPolynomial.weightedTotalDegree_rename_of_injective`, `DirectSum.toAddMonoidAlgebra_pow`, `MvPolynomial.range_mapAlgHom`, `MvPolynomial.irreducible_sumSMulXSMulY`, `MvPolynomial.mem_ideal_span_monomial_image`, `antipode_single`, `decomposeAux_eq_decompose`, `MvPolynomial.rename_toMvPolynomial`, `MvPolynomial.aeval_rename`, `WittVector.bind₁_frobeniusPolyRat_wittPolynomial`, `MvPolynomial.optionEquivLeft_symm_C_X`, `WittVector.aeval_verschiebungPoly`, `MvPolynomial.eval₂Hom_bind₁`, `Polynomial.homogenize_X`, `MvPolynomial.finSuccEquiv_X_zero`, `MvPolynomial.degreeOf_eq_natDegree`, `symm_mapAlgEquiv`, `MonomialOrder.sPolynomial_mem_sup_ideal`, `MvPolynomial.bind₁_X_right`, `MvPolynomial.coeff_rename_eq_zero`, `lift_unique`, `MvPolynomial.eval₂Hom_C_left`, `MvPolynomial.transcendental_supported_polynomial_aeval_X_iff`, `MvPolynomial.aeval_monomial`, `lift_def`, `StandardEtalePresentation.toPresentation_relation`, `DividedPowerAlgebra.dp_smul`, `Polynomial.toMvPolynomial_injective`, `MvPolynomial.coeff_eval_eq_eval_coeff`, `singleZeroAlgHom_apply`, `MvPolynomial.C_pow`, `LinearMap.polyCharpoly_natDegree`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_val`, `Algebra.Generators.self_algebra_algebraMap`, `MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse`, `Polynomial.coe_toLaurentAlg`, `WittVector.mul_polyOfInterest_aux3`, `MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix`, `Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul`, `scalarTensorEquiv_tmul`, `MvRatFunc.rank_eq_max_lift`, `MvPolynomial.aeval_prod`, `MvPolynomial.homogeneousSubmodule_mul`, `Matrix.toMvPolynomial_mul`, `Polynomial.Bivariate.pderiv_one_equivMvPolynomial`, `MvPolynomial.exists_restrict_to_vars`, `wittStructureInt_rename`, `MvPolynomial.algebraTensorAlgEquiv_symm_monomial`, `FirstOrder.Ring.mvPolynomial_zeroLocus_definable`, `MvPolynomial.aevalTower_algebraMap`, `MvPolynomial.optionEquivLeft_elim_eval`, `MvPolynomial.optionEquivLeft_symm_X`, `MvPolynomial.renameEquiv_symm`, `MvPolynomial.eval_expand`, `MvPolynomial.aeval_comp_toMvPolynomial`, `MvPolynomial.supportedEquivMvPolynomial_symm_C`, `Polynomial.toLaurentAlg_apply`, `MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset`, `MvPolynomial.eval₂AlgHom_apply`, `MvPolynomial.tensorEquivSum_X_tmul_one`, `MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet`, `symm_commRingEquiv`, `MvPolynomial.expand_mul_eq_comp`, `MvPolynomial.eval₂_pUnitAlgEquiv`, `MvPolynomial.killCompl_monomial`, `Polynomial.map_map_freeMonic`, `MvPolynomial.supported_eq_range_rename`, `LaurentPolynomial.toLaurent_reverse`, `MvPolynomial.rename_hsymm`, `MonomialOrder.sPolynomial_decomposition'`, `addMonoidAlgebraAlgEquivDirectSum_apply`, `MvPolynomial.transcendental_supported_X`, `DividedPowerAlgebra.dp_add`, `MvPolynomial.aeval_natDegree_le`, `grade.gradedMonoid`, `MvPolynomial.optionEquivLeft_symm_C_C`, `support_gen_of_gen'`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `Algebra.Generators.Hom.algebraMap_toAlgHom`, `WittVector.coeff_frobenius`, `Algebra.Generators.comp_σ`, `DividedPowerAlgebra.dp_null_of_ne_zero`, `MvPolynomial.tensorEquivSum_C_tmul_C`, `MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous`, `DividedPowerAlgebra.mkRingHom_C`, `MvPolynomial.instIsDomainOfIsCancelAdd`, `MvPowerSeries.subst_coe`, `isLocalHom_singleZeroAlgHom`, `MvPolynomial.mapEquivMonic_symm_map_algebraMap`, `MvPolynomial.coe_aeval_eq_eval`, `DividedPowerAlgebra.prod_dp`, `LaurentPolynomial.invert_C`, `exists_integral_inj_algHom_of_fg`, `MvPolynomial.instIsLocalHomRingHomC`, `MvPolynomial.coeff_add_pow`, `curryAlgEquiv_single`, `Matrix.charpoly.univ_coeff_card`, `Polynomial.Bivariate.equivMvPolynomial_C_C`, `DividedPowerAlgebra.mkAlgHom_C`, `MvPolynomial.monomial_single_add`, `wittPolynomial_eq_sum_C_mul_X_pow`, `Polynomial.homogenize_one`, `Algebra.Generators.ker_naive`, `instFreeMvPolynomialKaehlerDifferential`, `MvPolynomial.hom_bind₁`, `MvPolynomial.coeff_expand_zero`, `rank_mvPolynomial_mvPolynomial`, `MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton`, `Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`, `Matrix.mvPolynomialX_mapMatrix_aeval`, `MvPolynomial.algebraMap_def`, `MvPolynomial.supported_eq_vars_subset`, `DividedPowerAlgebra.embed_def`, `MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm`, `Polynomial.aeval_homogenize_of_eq_one`, `LaurentPolynomial.invert_comp_C`, `MvPolynomial.rename_eq`, `LaurentPolynomial.antipode_C_mul_T`, `MvPolynomial.totalDegree_coeff_optionEquivLeft_le`, `freeAlgebra_lift_of_surjective_of_closure`, `mapAlgEquiv_apply`, `MvPolynomial.eval₂Hom_smul`, `MvPolynomial.mapEquivMonic_symm_map`, `MvPolynomial.mem_ideal_span_X_image`, `MvPolynomial.isHomogeneous_X_pow`, `Algebra.SubmersivePresentation.basisDeriv_apply`, `MvPolynomial.bind₁_monomial`, `LinearMap.polyCharpoly_coeff_eval`, `MonomialOrder.degree_smul_of_mem_nonZeroDivisors`, `Algebra.Presentation.mem_ker_naive`, `MvPolynomial.C_eq_smul_one`, `MvPolynomial.coeff_killCompl`, `MvPolynomial.esymmAlgHom_surjective`, `MvPolynomial.aevalTower_ofNat`, `MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range`, `MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid`, `MvPolynomial.esymmAlgEquiv_symm_apply`, `instIsPushoutFractionRingMvPolynomial_1`, `MvPolynomial.rename_surjective`, `MvPolynomial.eval₂Hom_comp_expand`, `Polynomial.toMvPolynomial_C`, `MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero`, `Algebra.Generators.Hom.equivAlgHom_apply_coe`, `Algebra.Generators.C_mul_X_sub_one_mem_ker`, `MvPolynomial.universalFactorizationMapPresentation_jacobian`, `instIsDomainOfIsCancelAddOfUniqueSums`, `DividedPowerAlgebra.dp_eq_mkRingHom`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap`, `LaurentPolynomial.invert_T`, `MvPolynomial.esymmAlgHom_injective`, `MvPolynomial.commAlgEquiv_C_X`, `MvPolynomial.expand_zero_apply`, `Polynomial.coeff_freeMonic`, `Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'`, `vaddAssocClass_addMonoidAlgebra`, `MvPolynomial.renameSymmetricSubalgebra_apply_coe`, `Algebra.FinitePresentation.iff_quotient_mvPolynomial'`, `MvPolynomial.coe_mapEquivMonic_comp`, `MvPolynomial.transcendental_supported_polynomial_aeval_X`, `instIsPushoutFractionRingMvPolynomial`, `LaurentPolynomial.involutive_invert`, `MvPolynomial.eval_polynomial_eval_finSuccEquiv`, `MvPolynomial.constantCoeff_comp_algebraMap`, `LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly`, `DividedPowerAlgebra.dp_null`, `MvPolynomial.pderiv_inl_universalFactorizationMap_X`, `MvPolynomial.instFaithfulSMul`, `MvPolynomial.rename_id`, `Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val`, `MvPolynomial.idealOfVars_fg`, `MvPolynomial.rTensorAlgHom_apply_eq`
`single` 📖	CompOp	93 math math: `singleHom_apply`, `mul_single_apply`, `liftNCRingHom_single`, `supDegree_single`, `comul_single`, `mapDomainAddEquiv_single`, `mapAlgHom_single`, `Polynomial.toFinsupp_monomial`, `single_apply`, `map_single`, `opRingEquiv_symm_single`, `intCast_def`, `counit_single`, `toDirectSum_single`, `single_commute_single`, `LieAlgebra.LoopAlgebra.toFinsupp_symm_single`, `Polynomial.ofFinsupp_single`, `lsingle_apply`, `of_apply`, `single_add`, `mapAddEquiv_single`, `smul_single`, `support_mul_single_subset`, `commAlgEquiv_single_single`, `support_single_mul_subset`, `domCongr_single`, `Polynomial.toFinsupp_X_pow`, `prod_single`, `mul_def`, `coe_algebraMap`, `commRingEquiv_single_single`, `mul_single_zero_apply`, `lift_single`, `lift_symm_apply`, `support_mul_single_eq_image`, `LaurentPolynomial.single_eq_C`, `single_zero_comm`, `singleAddHom_apply`, `supported_eq_span_single`, `mapRingHom_single`, `natCast_def`, `leadingCoeff_single`, `LieAlgebra.LoopAlgebra.toFinsupp_single_tmul`, `single_mul_apply`, `single_mul_apply_of_not_exists_add`, `LaurentPolynomial.single_eq_C_mul_T`, `single_mem_grade`, `of'_apply`, `liftNC_single`, `opRingEquiv_single`, `smul_single'`, `ofMagma_apply`, `mul_single_apply_aux`, `Polynomial.toFinsupp_X`, `single_mul_single`, `erase_single`, `tensorEquiv_symm_single`, `DirectSum.toAddMonoidAlgebra_of`, `curryRingEquiv_symm_single`, `mapDomainRingEquiv_single`, `single_eq_zero`, `LaurentPolynomial.smeval_single`, `single_zero`, `curryAlgEquiv_symm_single`, `algHom_ext_iff`, `basis_apply`, `LaurentPolynomial.single_zero_one_eq_one`, `scalarTensorEquiv_symm_single`, `support_single_mul`, `support_single_mul_eq_image`, `single_pow`, `single_zero_mul_apply`, `supDegree_single_ne_zero`, `Polynomial.toFinsupp_C_mul_X_pow`, `single_neg`, `single_mul_apply_aux`, `curryRingEquiv_single`, `Polynomial.toFinsupp_C_mul_X`, `antipode_single`, `lift_unique`, `singleZeroAlgHom_apply`, `mapDomain_single`, `sum_single`, `single_mem_gradeBy`, `single_commute`, `sum_single_index`, `curryAlgEquiv_single`, `mul_single_apply_of_not_exists_add`, `one_def`, `support_mul_single`, `mapRingEquiv_single`, `Polynomial.toFinsupp_C`, `comapDomain_single_map`
`singleAddHom` 📖	CompOp	3 math math: `singleZeroRingHom_apply`, `singleAddHom_apply`, `addHom_ext'_iff`
`singleHom` 📖	CompOp	1 math math: `singleHom_apply`
`singleZeroRingHom` 📖	CompOp	3 math math: `singleZeroRingHom_apply`, `isLocalHom_singleZeroRingHom`, `ringHom_ext'_iff`
`smulZeroClass` 📖	CompOp	25 math math: `isScalarTower_self`, `Polynomial.homogenize_smul`, `MvPolynomial.smul_monomial`, `smulCommClass`, `smul_single`, `smul_apply`, `smulCommClass_symm_self`, `isScalarTower`, `MvPolynomial.coeff_smul`, `MvPolynomial.constantCoeff_smul`, `faithfulSMul`, `Polynomial.ofFinsupp_smul`, `coeff_smul`, `liftNC_smul`, `smul_single'`, `MvPolynomial.support_smul_eq`, `Polynomial.toFinsupp_smul`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `LaurentPolynomial.smul_eq_C_mul`, `MvPolynomial.totalDegree_smul_le`, `ofCoeff_smul`, `MvPolynomial.support_smul`, `isCentralScalar`, `smulCommClass_self`
`unexpander` 📖	CompOp	—
`unique` 📖	CompOp	—
`uniqueRingEquiv` 📖	CompOp	2 math math: `uniqueRingEquiv_apply`, `uniqueRingEquiv_symm_apply`
`update` 📖	CompOp	2 math math: `ofCoeff_update`, `coeff_update`
`zero` 📖	CompOp	95 math math: `sup_support_list_prod_le`, `MvPowerSeries.truncFinset_one`, `MvPolynomial.one_def`, `KaehlerDifferential.mvPolynomialBasis_repr_D_X`, `Algebra.Generators.toAlgHom_ofComp_localizationAway`, `of'_divOf`, `Algebra.Presentation.localizationAway_relation`, `mapDomain_one`, `MvPolynomial.pderiv_one`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `MvPolynomial.coe_one`, `LaurentPolynomial.invOf_T`, `MvPolynomial.coeffs_one`, `MvPolynomial.coeffs_one_of_nontrivial`, `MvPolynomial.coe_eq_one_iff`, `MvPolynomial.totalDegree_list_prod`, `MvPowerSeries.trunc_one`, `Algebra.SubmersivePresentation.ofSubsingleton_relation`, `DirectSum.toAddMonoidAlgebra_one`, `LaurentPolynomial.T_zero`, `Algebra.SubmersivePresentation.jacobianRelations_spec`, `MvPolynomial.IsSymmetric.one`, `Polynomial.ofFinsupp_eq_one`, `MvPolynomial.C_1`, `MvPolynomial.eval₂_one`, `MvPolynomial.pderiv_X`, `IsLocalization.Away.mvPolynomialQuotientEquiv_apply`, `MvPolynomial.isWeightedHomogeneous_one`, `MvPolynomial.tensorEquivSum_one_tmul_C`, `Polynomial.ofFinsupp_one`, `MvPolynomial.pderiv_def`, `le_inf_support_list_prod`, `Polynomial.toFinsupp_one`, `Algebra.Generators.ker_localizationAway`, `MvPolynomial.psumPart_zero`, `Algebra.Generators.comp_localizationAway_ker`, `MvPolynomial.mul_esymm_eq_sum`, `MvPolynomial.universalFactorizationMapPresentation_relation`, `MvPolynomial.coeff_one`, `monic_one`, `MvPolynomial.msymm_zero`, `MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap`, `MvPolynomial.degrees_one`, `MvPolynomial.divMonomial_monomial`, `Algebra.Generators.cMulXSubOneCotangent_eq`, `support_one_subset`, `MonomialOrder.degree_one`, `MvPolynomial.isHomogeneous_one`, `Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs`, `MvPolynomial.hsymmPart_zero`, `MvPolynomial.ker_eval₂Hom_universalFactorizationMap`, `Polynomial.toFinsupp_eq_one`, `MvPolynomial.support_one`, `MvPolynomial.vars_one`, `MvPolynomial.degreeOf_one`, `Algebra.Presentation.relation_comp_localizationAway_inl`, `MvPolynomial.tensorEquivSum_C_tmul_one`, `MvPolynomial.hsymm_zero`, `Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one`, `MvPolynomial.totalDegree_one`, `Polynomial.toLaurent_one`, `LaurentPolynomial.smeval_one`, `LaurentPolynomial.single_zero_one_eq_one`, `MvPolynomial.pderiv_inr_universalFactorizationMap_X`, `liftNC_one`, `MvPolynomial.esymmPart_zero`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `MvPolynomial.psum_eq_mul_esymm_sub_sum`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `WittVector.bind₁_onePoly_wittPolynomial`, `WittVector.wittOne_zero_eq_one`, `map_one`, `Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero`, `Algebra.SubmersivePresentation.ofSubsingleton_σ'`, `MvPolynomial.universalFactorizationMapPresentation_algebra_smul`, `MvPolynomial.tensorEquivSum_one_tmul_X`, `MvPolynomial.one_coeffsIn`, `MvPolynomial.universalFactorizationMapPresentation_val`, `MonomialOrder.monic_one`, `MvPolynomial.esymm_zero`, `StandardEtalePresentation.toPresentation_relation`, `MvPolynomial.pderiv_X_self`, `MvPowerSeries.trunc'_one`, `MonomialOrder.leadingCoeff_one`, `MvPolynomial.X_divMonomial`, `MvPolynomial.tensorEquivSum_X_tmul_one`, `MvPolynomial.coeff_zero_one`, `Matrix.charpoly.univ_coeff_card`, `toDirectSum_one`, `one_def`, `MvPolynomial.C_eq_smul_one`, `support_one`, `Algebra.Generators.C_mul_X_sub_one_mem_ker`, `Polynomial.coeff_freeMonic`, `MvPolynomial.pderiv_inl_universalFactorizationMap_X`
`«term__[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addHom_ext'` 📖	—	`AddMonoidHom.comp` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `singleAddHom`	—	—	`Finsupp.addHom_ext'`
`addHom_ext'_iff` 📖	mathematical	—	`AddMonoidHom.comp` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `singleAddHom`	—	`addHom_ext'`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coeffAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `coeffAddEquiv` `coeff`	—	—
`coeffAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `coeffAddEquiv` `ofCoeff`	—	—
`coeffEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `coeffEquiv` `coeff`	—	—
`coeffEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `coeffEquiv` `ofCoeff`	—	—
`coeff_add` 📖	mathematical	—	`coeff` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`coeff_eq_zero` 📖	mathematical	—	`coeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	—
`coeff_erase` 📖	mathematical	—	`coeff` `erase` `Finsupp.erase` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coeff_finsuppSum` 📖	mathematical	—	`coeff` `Finsupp.sum` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`map_finsuppSum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`coeff_inj` 📖	mathematical	—	`coeff`	—	`coeff_injective`
`coeff_injective` 📖	mathematical	—	`AddMonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff`	—	`Equiv.injective`
`coeff_neg` 📖	mathematical	—	`coeff` `Ring.toSemiring` `AddMonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instNeg` `Ring.toAddCommGroup`	—	—
`coeff_ofCoeff` 📖	mathematical	—	`coeff` `ofCoeff`	—	—
`coeff_smul` 📖	mathematical	—	`coeff` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero` `Finsupp.smulZeroClass`	—	—
`coeff_sub` 📖	mathematical	—	`coeff` `Ring.toSemiring` `AddMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addAddCommGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instSub` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	—
`coeff_sum` 📖	mathematical	—	`coeff` `Finset.sum` `AddMonoidAlgebra` `addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`coeff_update` 📖	mathematical	—	`coeff` `update` `Finsupp.update` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coeff_zero` 📖	mathematical	—	`coeff` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero`	—	—
`curryRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `semiring` `instMul` `Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `curryRingEquiv` `single`	—	`Finsupp.curry_single`
`curryRingEquiv_symm_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `semiring` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `curryRingEquiv` `single`	—	`Finsupp.uncurry_single`
`erase_single` 📖	mathematical	—	`erase` `single` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	`Finsupp.erase_single`
`erase_zero` 📖	mathematical	—	`erase` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	`Finsupp.erase_of_notMem_support` `Finset.notMem_empty`
`exists` 📖	mathematical	—	`AddMonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `ofCoeff`	—	`Equiv.exists_congr_left`
`ext` 📖	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike`	—	—	`Finsupp.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike`	—	`ext`
`forall` 📖	mathematical	—	`ofCoeff`	—	`Equiv.forall_congr_left`
`induction_linear` 📖	—	`AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `single`	—	—	`Finsupp.induction_linear`
`induction_on` 📖	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `AddMonoidAlgebra` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—	`Finsupp.induction_linear` `smul_single` `mul_one` `Finsupp.single_zero`
`instIsCancelAdd` 📖	mathematical	—	`IsCancelAdd` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	—
`intCast_def` 📖	mathematical	—	`AddMonoidAlgebra` `Ring.toSemiring` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `nonAssocRing` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `Ring.toAddGroupWithOne`	—	—
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `MulOpposite`	—	—
`isLocalHom_singleZeroRingHom` 📖	mathematical	—	`IsLocalHom` `AddMonoidAlgebra` `RingHom` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `RingHom.instFunLike` `singleZeroRingHom`	—	`isUnit_iff_exists` `single_zero_mul_apply` `Finsupp.single_eq_same` `mul_single_zero_apply`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `Finsupp.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_def` `Finsupp.sum_apply` `single_apply`
`mul_apply_antidiagonal` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finset.sum_filter` `Finset.sum_product` `Finset.sum_congr` `Finset.ext` `Finset.mem_filter` `Finset.mem_product` `Finset.sum_subset` `Finset.filter_subset` `MulZeroClass.zero_mul` `Finset.filter.congr_simp` `Finsupp.mem_support_iff` `MulZeroClass.mul_zero`
`mul_apply_left` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Finsupp.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`mul_apply` `Finset.sum_congr` `eq_neg_add_iff_add_eq` `Finset.sum_ite_eq'` `Finsupp.mem_support_iff` `MulZeroClass.mul_zero`
`mul_apply_right` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Finsupp.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`mul_apply` `Finsupp.sum_comm` `Finset.sum_congr` `eq_add_neg_iff_add_eq` `Finset.sum_ite_eq'` `Finsupp.mem_support_iff` `MulZeroClass.zero_mul`
`mul_def` 📖	mathematical	—	`AddMonoidAlgebra` `instMul` `Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addAddCommMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mul_single_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`mul_single_apply_aux` `Finsupp.mem_support_iff` `eq_add_neg_iff_add_eq`
`mul_single_apply_aux` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `Finset.sum_congr` `Finsupp.sum_eq_single` `MulZeroClass.zero_mul`
`mul_single_apply_of_not_exists_add` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `single`	—	`mul_apply` `Finsupp.sum_single_index` `Finsupp.sum_fun_zero`
`mul_single_zero_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `single` `AddZero.toZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_single_apply_aux` `Finsupp.mem_support_iff` `add_zero`
`natCast_def` 📖	mathematical	—	`AddMonoidAlgebra` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `nonAssocSemiring` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `Semiring.toNonAssocSemiring`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addAddCommGroup` `Ring.toAddCommGroup`	—	—
`nontrivial` 📖	mathematical	—	`Nontrivial` `AddMonoidAlgebra`	—	—
`of'_apply` 📖	mathematical	—	`of'` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`of'_commute` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero`	`Commute` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `of'`	—	`single_commute` `Commute.one_left`
`of'_eq_of` 📖	mathematical	—	`of'` `DFunLike.coe` `MonoidHom` `Multiplicative` `AddMonoidAlgebra` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—
`ofCoeff_add` 📖	mathematical	—	`ofCoeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	—
`ofCoeff_coeff` 📖	mathematical	—	`ofCoeff` `coeff`	—	—
`ofCoeff_eq_zero` 📖	mathematical	—	`ofCoeff` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero`	—	—
`ofCoeff_erase` 📖	mathematical	—	`ofCoeff` `Finsupp.erase` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `erase`	—	—
`ofCoeff_finsuppSum` 📖	mathematical	—	`ofCoeff` `Finsupp.sum` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidAlgebra` `addAddCommMonoid`	—	`map_finsuppSum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofCoeff_inj` 📖	mathematical	—	`ofCoeff`	—	`ofCoeff_injective`
`ofCoeff_injective` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `ofCoeff`	—	`Equiv.injective`
`ofCoeff_neg` 📖	mathematical	—	`ofCoeff` `Ring.toSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidAlgebra` `NegZeroClass.toNeg` `addAddCommGroup`	—	—
`ofCoeff_smul` 📖	mathematical	—	`ofCoeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass`	—	—
`ofCoeff_sub` 📖	mathematical	—	`ofCoeff` `Ring.toSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instSub` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addAddCommGroup`	—	—
`ofCoeff_sum` 📖	mathematical	—	`ofCoeff` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidAlgebra` `addAddCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofCoeff_update` 📖	mathematical	—	`ofCoeff` `Finsupp.update` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `update`	—	—
`ofCoeff_zero` 📖	mathematical	—	`ofCoeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	—
`ofMagma_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `Multiplicative` `AddMonoidAlgebra` `Multiplicative.mul` `instMul` `MulHom.funLike` `ofMagma` `single` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`of_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `AddMonoidAlgebra` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `single` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`of_injective` 📖	mathematical	—	`Multiplicative` `AddMonoidAlgebra` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`MonoidAlgebra.of_injective`
`one_def` 📖	mathematical	—	`AddMonoidAlgebra` `zero` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`prod_single` 📖	mathematical	—	`Finset.prod` `AddMonoidAlgebra` `CommSemiring.toSemiring` `CommSemiring.toCommMonoid` `commSemiring` `single` `Finset.sum`	—	`Finset.cons_induction_on` `Finset.prod_cons` `single_mul_single` `Finset.sum_cons`
`ringHom_ext` 📖	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`RingHom.coe_addMonoidHom_injective` `Finsupp.addHom_ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `single_mul_single` `zero_add` `mul_one`
`ringHom_ext'` 📖	—	`RingHom.comp` `AddMonoidAlgebra` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `singleZeroRingHom` `MonoidHom.comp` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHomClass.toMonoidHom` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `of`	—	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ringHom_ext` `RingHom.congr_fun` `DFunLike.congr_fun`
`ringHom_ext'_iff` 📖	mathematical	—	`RingHom.comp` `AddMonoidAlgebra` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `singleZeroRingHom` `MonoidHom.comp` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHomClass.toMonoidHom` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `of`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ringHom_ext'`
`singleAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `AddMonoidHom.instFunLike` `singleAddHom` `single`	—	—
`singleHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `AddMonoidAlgebra` `MulOneClass.toMulOne` `Prod.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Multiplicative.mulOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `singleHom` `single` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`singleZeroRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `RingHom.instFunLike` `singleZeroRingHom` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `AddMonoidHom.toZeroHom` `singleAddHom`	—	—
`single_add` 📖	mathematical	—	`single` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	`Finsupp.single_add`
`single_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `single`	—	`Finsupp.single_apply`
`single_commute` 📖	mathematical	`AddCommute` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Commute` `AddMonoidAlgebra` `instMul` `single`	—	`addHom_ext'` `AddMonoidHom.ext` `single_commute_single`
`single_commute_single` 📖	mathematical	`AddCommute` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Commute` `AddMonoidAlgebra` `instMul` `single`	—	`single_mul_single` `AddCommute.eq` `Commute.eq`
`single_eq_zero` 📖	mathematical	—	`single` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finsupp.single_eq_zero`
`single_mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`single_mul_apply_aux` `Finsupp.mem_support_iff` `eq_neg_add_iff_add_eq`
`single_mul_apply_aux` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finsupp.sum_single_index` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `Finset.sum_congr` `Finsupp.sum_eq_single` `MulZeroClass.mul_zero`
`single_mul_apply_of_not_exists_add` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `single`	—	`mul_apply` `Finsupp.sum_single_index` `Finsupp.sum_fun_zero`
`single_mul_single` 📖	mathematical	—	`AddMonoidAlgebra` `instMul` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mul_def` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `MulZeroClass.zero_mul`
`single_ne_zero` 📖	—	—	—	—	`single_eq_zero`
`single_neg` 📖	mathematical	—	`single` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidAlgebra` `addAddCommGroup`	—	`Finsupp.single_neg`
`single_pow` 📖	mathematical	—	`AddMonoidAlgebra` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `single` `AddMonoid.toNSMul`	—	`pow_zero` `zero_nsmul` `pow_succ` `single_mul_single` `succ_nsmul`
`single_zero` 📖	mathematical	—	`single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid`	—	`Finsupp.single_zero`
`single_zero_comm` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `single` `AddZero.toZero`	—	`single_commute` `AddCommute.zero_left` `Commute.all`
`single_zero_mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `single` `AddZero.toZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`single_mul_apply_aux` `Finsupp.mem_support_iff` `zero_add`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass`	—	—
`smul_single` 📖	mathematical	—	`AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext` `Finsupp.smul_single`
`smul_single'` 📖	mathematical	—	`AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smul_single`
`sum_single` 📖	mathematical	—	`Finsupp.sum` `AddMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addAddCommMonoid` `single`	—	`Finsupp.sum_single`
`sum_single_index` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `single`	—	`Finsupp.sum_single_index`
`uniqueRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `uniqueRingEquiv` `Finsupp` `AddZero.toZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finsupp.instFunLike` `Unique.instInhabited`	—	—
`uniqueRingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Distrib.toAdd` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `uniqueRingEquiv` `Equiv` `Finsupp` `AddZero.toZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Equiv.instEquivLike` `Equiv.symm` `Finsupp.equivFunOnFinite` `uniqueElim`	—	—

MonoidAlgebra

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	11 math math: `ofCoeff_sub`, `coeff_neg`, `ofCoeff_neg`, `FreeLieAlgebra.Rel.neg`, `FreeLieAlgebra.Rel.subRight`, `FreeLieAlgebra.Rel.subLeft`, `map_sub`, `single_neg`, `map_neg`, `neg_apply`, `coeff_sub`
`addCommMonoid` 📖	CompOp	86 math math: `Representation.ofMulActionSelfAsModuleEquiv_symm_apply`, `supportedEquivFinsupp_symm_apply_coe_apply`, `supported_eq_span_single`, `instIsCocomm`, `tensorEquiv.invFun_tmul`, `liftNC_mul`, `mul_def`, `instIsCancelAdd`, `coeff_smul`, `single_eq_zero`, `smulCommClass`, `of_mem_span_of_iff`, `coe_liftNCAlgHom`, `smulCommClass_self`, `distribMulActionHom_ext'_iff`, `FreeLieAlgebra.liftAux_map_smul`, `scalarTensorEquiv_tmul`, `instFree`, `basis_apply`, `AddMonoidAlgebra.tensorEquiv.invFun_tmul`, `singleAddHom_apply`, `mem_span_support`, `faithfulSMul`, `erase_zero`, `lsingle_apply`, `tensorEquiv_symm_single`, `coeffLinearEquiv_symm_apply`, `ofCoeff_finsuppSum`, `ofCoeff_eq_zero`, `smul_single`, `coe_add`, `moduleFinite`, `smul_of`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `Representation.ofMulActionSelfAsModuleEquiv_apply`, `liftNC_single`, `smul_single'`, `map_zero`, `tensorEquiv_tmul`, `sum_single`, `comapDomain_single_of_not_mem_range`, `smul_apply`, `coeffLinearEquiv_apply`, `erase_single`, `coeff_finsuppSum`, `lhom_ext'_iff`, `supportedEquivFinsupp_apply_support_val`, `ofCoeff_zero`, `scalarTensorEquiv_symm_single`, `coeffAddEquiv_symm_apply`, `comul_single`, `supportedEquivFinsupp_apply_apply`, `coeff_zero`, `comapDomain_add`, `comapDomain_zero`, `singleOneRingHom_apply`, `supported_eq_map`, `ofCoeff_sum`, `smulCommClass_symm_self`, `mapDomain_zero`, `FreeLieAlgebra.Rel.smulOfTower`, `single_zero`, `liftNC_smul`, `coeffAddEquiv_apply`, `instIsTorsionFree`, `coeff_eq_zero`, `single_add`, `mem_supported`, `isScalarTower_self`, `ofCoeff_smul`, `supported_mono`, `lift_def`, `isCentralScalar`, `isScalarTower`, `addHom_ext'_iff`, `mapDomain_sum`, `coeff_sum`, `liftNC_one`, `counit_single`, `coeff_add`, `map_add`, `comapDomainAddMonoidHom_apply`, `mem_supported'`, `mapDomain_add`, `map_sum`, `ofCoeff_add`
`coeff` 📖	CompOp	23 math math: `coeff_smul`, `coeff_update`, `coeff_neg`, `ofCoeff_coeff`, `coeff_comapDomain`, `coeff_injective`, `coeffLinearEquiv_apply`, `coeff_ofCoeff`, `coeff_finsuppSum`, `supportedEquivFinsupp_apply_support_val`, `supportedEquivFinsupp_apply_apply`, `coeff_zero`, `coeff_inj`, `coeff_map`, `coeffAddEquiv_apply`, `coeff_eq_zero`, `mem_supported`, `coeffEquiv_apply`, `coeff_sum`, `coeff_add`, `mem_supported'`, `coeff_sub`, `coeff_erase`
`coeffAddEquiv` 📖	CompOp	2 math math: `coeffAddEquiv_symm_apply`, `coeffAddEquiv_apply`
`coeffEquiv` 📖	CompOp	2 math math: `coeffEquiv_symm_apply`, `coeffEquiv_apply`
`commRing` 📖	CompOp	2 math math: `CommRingCat.monoidAlgebra_map`, `CommRingCat.monoidAlgebra_obj`
`commSemiring` 📖	CompOp	6 math math: `instIsPushout`, `mvPolynomial_aeval_of_surjective_of_closure`, `isScalarTower_monoidAlgebra`, `instIsPushout'`, `algebraMap_def`, `prod_single`
`curryRingEquiv` 📖	CompOp	2 math math: `curryRingEquiv_symm_single`, `curryRingEquiv_single`
`distribSMul` 📖	CompOp	—
`erase` 📖	CompOp	4 math math: `erase_zero`, `erase_single`, `ofCoeff_erase`, `coeff_erase`
`inhabited` 📖	CompOp	—
`instCoeFun` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instMul` 📖	CompOp	61 math math: `mapDomainRingEquiv_single`, `liftNC_mul`, `mul_def`, `opRingEquiv_single`, `mapDomainRingEquiv_trans`, `single_one_mul_apply`, `mapRingEquiv_single`, `opRingEquiv_symm_apply`, `uniqueRingEquiv_apply`, `mapRangeRingEquiv_single`, `single_mul_apply`, `single_algebraMap_eq_algebraMap_mul_of`, `symm_mapRangeRingEquiv`, `support_mul_single_eq_image`, `mapRingEquiv_trans`, `single_mul_apply_aux`, `ofMagma_apply`, `symm_commRingEquiv`, `opRingEquiv_symm_single`, `curryRingEquiv_symm_single`, `FreeLieAlgebra.liftAux_map_mul`, `mul_apply_mul_eq_mul_of_uniqueMul`, `single_mul_single`, `support_mul_single_subset`, `instIsCancelMulZeroOfIsCancelAddOfUniqueProds`, `single_commute`, `instNoZeroDivisorsOfUniqueProds`, `single_one_comm`, `mapRingEquiv_apply`, `mapRangeRingEquiv_apply`, `instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds`, `support_mul_single`, `mul_single_apply_of_not_exists_mul`, `mul_single_one_apply`, `mapRangeRingEquiv_trans`, `support_single_mul_eq_image`, `curryRingEquiv_single`, `of_commute`, `uniqueRingEquiv_symm_apply`, `symm_mapRingEquiv`, `support_single_mul`, `mul_apply`, `map_mul`, `mapDomainRingEquiv_apply`, `instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds`, `single_commute_single`, `single_eq_algebraMap_mul_of`, `GroupAlgebra.mul_average_left`, `mul_apply_right`, `symm_mapDomainRingEquiv`, `mul_single_apply`, `support_single_mul_subset`, `mul_apply_antidiagonal`, `mapDomain_mul`, `single_mul_apply_of_not_exists_mul`, `support_mul`, `opRingEquiv_apply`, `commRingEquiv_single_single`, `GroupAlgebra.mul_average_right`, `mul_single_apply_aux`, `mul_apply_left`
`mul'` 📖	CompOp	—
`nonAssocRing` 📖	CompOp	1 math math: `intCast_def`
`nonAssocSemiring` 📖	CompOp	60 math math: `exists_leftInverse_of_injective`, `Representation.ofMulActionSelfAsModuleEquiv_symm_apply`, `mapRangeRingHom_single`, `algHom_ext'_iff`, `mapDomainRingHom_id`, `mem_adjoin_support`, `of_mem_span_of_iff`, `support_gen_of_gen'`, `LinearMap.sumOfConjugatesEquivariant_apply`, `mapRingHom_apply`, `mapRingHom_comp`, `mvPolynomial_aeval_of_surjective_of_closure`, `toRingHom_mapRangeAlgHom`, `single_algebraMap_eq_algebraMap_mul_of`, `liftNCRingHom_single`, `mem_span_support`, `coe_mapRangeRingHom`, `isLocalHom_singleOneRingHom`, `toRingHom_mapRingEquiv`, `mapRangeRingHom_comp_mapDomainRingHom`, `mapRingHom_comp_mapDomainRingHom`, `freeAlgebra_lift_of_surjective_of_closure`, `ringHom_ext_iff`, `mapRangeRingHom_comp_algebraMap`, `toRingHom_mapDomainRingEquiv`, `exists_finset_adjoin_eq_top`, `smul_of`, `Representation.ofMulActionSelfAsModuleEquiv_apply`, `LinearMap.equivariantProjection_condition`, `Representation.asModuleEquiv_symm_map_rho`, `Representation.asAlgebraHom_of`, `singleHom_apply`, `support_gen_of_gen`, `LinearMap.equivariantProjection_apply`, `mapRingHom_id`, `of_commute`, `LinearMap.conjugate_i`, `mem_ideal_span_of_image`, `lift_mapRangeRingHom_algebraMap`, `of_injective`, `mapDomainRingHom_comp`, `mapRingHom_single`, `equivariantOfLinearOfComm_apply`, `singleOneRingHom_apply`, `lift_mapRingHom_algebraMap`, `toRingHom_mapRangeRingEquiv`, `ringHom_ext'_iff`, `single_eq_algebraMap_mul_of`, `mapRingHom_comp_algebraMap`, `mapRangeRingHom_id`, `mapDomainRingHom_apply`, `mapDomainRingHom_comp_algebraMap`, `natCast_def`, `mapRangeRingHom_comp`, `toRingHom_mapAlgHom`, `of_apply`, `lift_of`, `mapRangeRingHom_apply`, `coe_mapRingHom`, `lift_unique'`
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalNonAssocSemiring` 📖	CompOp	59 math math: `mapDomainRingEquiv_single`, `liftMagma_apply_apply`, `opRingEquiv_single`, `mapDomainRingEquiv_trans`, `symm_mapAddEquiv`, `FreeNonUnitalNonAssocAlgebra.of_comp_lift`, `mapRingEquiv_single`, `opRingEquiv_symm_apply`, `FreeLieAlgebra.Rel.addLeft`, `symm_mapDomainAddEquiv`, `uniqueRingEquiv_apply`, `mapDomainNonUnitalRingHom_id`, `smulCommClass_self`, `FreeNonUnitalNonAssocAlgebra.lift_unique`, `mapDomainAddEquiv_single`, `mapRangeRingEquiv_single`, `FreeLieAlgebra.liftAux_map_smul`, `mapAddEquiv_trans`, `symm_mapRangeRingEquiv`, `mapRingEquiv_trans`, `symm_commRingEquiv`, `FreeLieAlgebra.liftAux_map_add`, `FreeNonUnitalNonAssocAlgebra.lift_symm_apply`, `opRingEquiv_symm_single`, `curryRingEquiv_symm_single`, `mapRangeAddEquiv_apply`, `FreeLieAlgebra.liftAux_map_mul`, `mapDomainAddEquiv_trans`, `mapRangeAddEquiv_trans`, `instIsCancelMulZeroOfIsCancelAddOfUniqueProds`, `FreeLieAlgebra.liftAux_spec`, `symm_mapRangeAddEquiv`, `instNoZeroDivisorsOfUniqueProds`, `mapRingEquiv_apply`, `mapRangeRingEquiv_apply`, `nonUnitalAlgHom_ext'_iff`, `mapDomainNonUnitalRingHom_apply`, `instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds`, `liftMagma_symm_apply`, `mapRangeRingEquiv_trans`, `curryRingEquiv_single`, `uniqueRingEquiv_symm_apply`, `mapAddEquiv_apply`, `symm_mapRingEquiv`, `mapAddEquiv_single`, `mapDomainNonUnitalAlgHom_apply`, `mapDomainNonUnitalRingHom_comp`, `smulCommClass_symm_self`, `mapDomainRingEquiv_apply`, `instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds`, `mapRangeAddEquiv_single`, `isScalarTower_self`, `symm_mapDomainRingEquiv`, `mapDomainAddEquiv_apply`, `FreeNonUnitalNonAssocAlgebra.lift_of_apply`, `opRingEquiv_apply`, `commRingEquiv_single_single`, `FreeNonUnitalNonAssocAlgebra.hom_ext_iff`, `FreeNonUnitalNonAssocAlgebra.lift_comp_of`
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	—
`of` 📖	CompOp	21 math math: `algHom_ext'_iff`, `mem_adjoin_support`, `of_mem_span_of_iff`, `support_gen_of_gen'`, `mvPolynomial_aeval_of_surjective_of_closure`, `single_algebraMap_eq_algebraMap_mul_of`, `mem_span_support`, `freeAlgebra_lift_of_surjective_of_closure`, `exists_finset_adjoin_eq_top`, `smul_of`, `Representation.asModuleEquiv_symm_map_rho`, `Representation.asAlgebraHom_of`, `support_gen_of_gen`, `of_commute`, `mem_ideal_span_of_image`, `of_injective`, `ringHom_ext'_iff`, `single_eq_algebraMap_mul_of`, `of_apply`, `lift_of`, `lift_unique'`
`ofCoeff` 📖	CompOp	21 math math: `ofCoeff_injective`, `forall`, `exists`, `ofCoeff_mapRange`, `ofCoeff_sub`, `ofCoeff_coeff`, `coeffLinearEquiv_symm_apply`, `coeffEquiv_symm_apply`, `ofCoeff_finsuppSum`, `ofCoeff_eq_zero`, `ofCoeff_neg`, `coeff_ofCoeff`, `ofCoeff_inj`, `supportedEquivFinsupp_apply_support_val`, `ofCoeff_zero`, `coeffAddEquiv_symm_apply`, `ofCoeff_sum`, `ofCoeff_smul`, `ofCoeff_erase`, `ofCoeff_update`, `ofCoeff_add`
`ofMagma` 📖	CompOp	3 math math: `ofMagma_apply`, `nonUnitalAlgHom_ext'_iff`, `liftMagma_symm_apply`
`one` 📖	CompOp	6 math math: `support_one_subset`, `map_one`, `mapDomain_one`, `one_def`, `liftNC_one`, `support_one`
`semiring` 📖	CompOp	114 math math: `finiteType_of_fg`, `exists_leftInverse_of_injective`, `Representation.ofMulActionSelfAsModuleEquiv_symm_apply`, `isLocalHom_algebraMap`, `Submodule.exists_isCompl`, `Representation.asAlgebraHom_single`, `algHom_ext'_iff`, `tensorEquiv.invFun_tmul`, `antipode_single`, `Subrepresentation.mem_ofSubmodule'_iff`, `domCongr_toAlgHom`, `Rep.to_Module_monoidAlgebra_map_aux`, `mem_adjoin_support`, `Representation.asAlgebraHom_def`, `lift_symm_apply`, `coe_liftNCAlgHom`, `support_gen_of_gen'`, `Representation.smul_ofModule_asModule`, `LinearMap.sumOfConjugatesEquivariant_apply`, `mapDomainBialgHom_comp`, `coe_algebraMap`, `mapDomain_algebraMap`, `Representation.ofMulAction_self_smul_eq_mul`, `mapAlgHom_single`, `mapDomainBialgHom_mapDomainBialgHom`, `Representation.single_smul`, `mapRangeAlgHom_single`, `mapRangeAlgEquiv_trans`, `domCongr_single`, `toRingHom_mapRangeAlgHom`, `scalarTensorEquiv_tmul`, `single_algebraMap_eq_algebraMap_mul_of`, `mapDomainAlgHom_id`, `mapDomainAlgHom_comp`, `isLocalHom_singleOneRingHom`, `Subrepresentation.mem_asSubmodule'_iff`, `Representation.asModuleEquiv_symm_map_smul`, `mapRangeAlgHom_apply`, `symm_mapRangeAlgEquiv`, `lift_unique`, `tensorEquiv_symm_single`, `symm_commRingEquiv`, `lift_apply'`, `Subrepresentation.submoduleSubrepresentationOrderIso_apply`, `mapDomainBialgHom_apply`, `freeAlgebra_lift_of_surjective_of_closure`, `Representation.asAlgebraHom_single_one`, `mapRangeRingHom_comp_algebraMap`, `Representation.isSimpleModule_iff_irreducible_ofModule`, `Representation.instIsScalarTowerMonoidAlgebraAsModule`, `curryRingEquiv_symm_single`, `Subrepresentation.mem_asSubmodule_iff`, `commAlgEquiv_single_single`, `isScalarTower_monoidAlgebra`, `isLocalHom_singleOneAlgHom`, `finiteType_iff_fg`, `exists_finset_adjoin_eq_top`, `Representation.ofMulActionSelfAsModuleEquiv_apply`, `LinearMap.conjugate_apply`, `LinearMap.equivariantProjection_condition`, `mapAlgHom_apply`, `Representation.asModuleEquiv_symm_map_rho`, `Representation.ofModule_asModule_act`, `tensorEquiv_tmul`, `Representation.asAlgebraHom_of`, `finiteType_iff_group_fg`, `domCongr_comp_lsingle`, `support_gen_of_gen`, `domCongr_symm`, `LinearMap.equivariantProjection_apply`, `GroupSMul.linearMap_apply`, `curryRingEquiv_single`, `scalarTensorEquiv_symm_single`, `LinearMap.conjugate_i`, `Representation.smul_tprod_one_asModule`, `algebraMap_def`, `mem_ideal_span_of_image`, `lift_apply`, `lift_mapRangeRingHom_algebraMap`, `equivariantOfLinearOfComm_apply`, `lift_mapRingHom_algebraMap`, `Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply`, `Representation.ofModule_asAlgebraHom_apply_apply`, `symm_commAlgEquiv`, `curryAlgEquiv_symm_single`, `mapAlgEquiv_apply`, `single_eq_algebraMap_mul_of`, `single_pow`, `domCongr_support`, `symm_mapAlgEquiv`, `Representation.asModuleEquiv_map_smul`, `singleOneAlgHom_apply`, `lift_def`, `Representation.smul_one_tprod_asModule`, `mapRingHom_comp_algebraMap`, `Representation.is_simple_module_iff_irreducible_ofModule`, `Subrepresentation.mem_ofSubmodule_iff`, `Representation.free_asModule_free`, `mapDomainAlgHom_apply`, `mapDomainRingHom_comp_algebraMap`, `Subrepresentation.subrepresentationSubmoduleOrderIso_apply`, `Representation.asAlgebraHom_mem_of_forall_mem`, `domCongr_refl`, `commRingEquiv_single_single`, `domCongr_apply`, `mapDomainBialgHom_id`, `instIsDomainOfIsCancelAddOfUniqueProds`, `lift_single`, `curryAlgEquiv_single`, `toRingHom_mapAlgHom`, `Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule`, `Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply`, `lift_of`, `lift_unique'`
`single` 📖	CompOp	87 math math: `mapDomainRingEquiv_single`, `comapDomain_single_map`, `mapRangeRingHom_single`, `Representation.asAlgebraHom_single`, `supported_eq_span_single`, `tensorEquiv.invFun_tmul`, `antipode_single`, `mul_def`, `opRingEquiv_single`, `single_one_mul_apply`, `single_eq_zero`, `mapRingEquiv_single`, `lift_symm_apply`, `mapDomainAddEquiv_single`, `mapRangeRingEquiv_single`, `coe_algebraMap`, `mapAlgHom_single`, `single_mul_apply`, `Representation.single_smul`, `mapRangeAlgHom_single`, `domCongr_single`, `basis_apply`, `single_algebraMap_eq_algebraMap_mul_of`, `liftNCRingHom_single`, `AddMonoidAlgebra.tensorEquiv.invFun_tmul`, `singleAddHom_apply`, `intCast_def`, `support_mul_single_eq_image`, `lsingle_apply`, `single_mul_apply_aux`, `ofMagma_apply`, `lift_unique`, `tensorEquiv_symm_single`, `opRingEquiv_symm_single`, `Representation.asAlgebraHom_single_one`, `ringHom_ext_iff`, `smul_single`, `curryRingEquiv_symm_single`, `commAlgEquiv_single_single`, `single_mul_single`, `smul_of`, `support_mul_single_subset`, `LinearMap.conjugate_apply`, `liftNC_single`, `smul_single'`, `single_commute`, `single_one_comm`, `sum_single`, `comapDomain_single_of_not_mem_range`, `singleHom_apply`, `map_single`, `support_mul_single`, `mul_single_apply_of_not_exists_mul`, `erase_single`, `mul_single_one_apply`, `support_single_mul_eq_image`, `GroupSMul.linearMap_apply`, `curryRingEquiv_single`, `scalarTensorEquiv_symm_single`, `comul_single`, `support_single_mul`, `mapAddEquiv_single`, `mapDomain_single`, `mapRingHom_single`, `single_zero`, `one_def`, `single_commute_single`, `curryAlgEquiv_symm_single`, `single_add`, `single_eq_algebraMap_mul_of`, `mapRangeAddEquiv_single`, `single_neg`, `single_pow`, `singleOneAlgHom_apply`, `mul_single_apply`, `single_apply`, `support_single_mul_subset`, `single_mul_apply_of_not_exists_mul`, `counit_single`, `commRingEquiv_single_single`, `natCast_def`, `lift_single`, `curryAlgEquiv_single`, `sum_single_index`, `of_apply`, `mul_single_apply_aux`, `prod_single`
`singleAddHom` 📖	CompOp	3 math math: `singleAddHom_apply`, `singleOneRingHom_apply`, `addHom_ext'_iff`
`singleHom` 📖	CompOp	1 math math: `singleHom_apply`
`singleOneRingHom` 📖	CompOp	5 math math: `isLocalHom_singleOneRingHom`, `CommRingCat.monoidAlgebra_map`, `singleOneRingHom_apply`, `ringHom_ext'_iff`, `CommRingCat.monoidAlgebra_obj`
`smulZeroClass` 📖	CompOp	16 math math: `coeff_smul`, `smulCommClass`, `smulCommClass_self`, `FreeLieAlgebra.liftAux_map_smul`, `faithfulSMul`, `smul_single`, `smul_of`, `smul_single'`, `smul_apply`, `smulCommClass_symm_self`, `FreeLieAlgebra.Rel.smulOfTower`, `liftNC_smul`, `isScalarTower_self`, `ofCoeff_smul`, `isCentralScalar`, `isScalarTower`
`unexpander` 📖	CompOp	—
`unique` 📖	CompOp	—
`uniqueRingEquiv` 📖	CompOp	2 math math: `uniqueRingEquiv_apply`, `uniqueRingEquiv_symm_apply`
`update` 📖	CompOp	2 math math: `coeff_update`, `ofCoeff_update`
`«term__[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addHom_ext'` 📖	—	`AddMonoidHom.comp` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addCommMonoid` `singleAddHom`	—	—	`Finsupp.addHom_ext'`
`addHom_ext'_iff` 📖	mathematical	—	`AddMonoidHom.comp` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addCommMonoid` `singleAddHom`	—	`addHom_ext'`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coeffAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `MonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `coeffAddEquiv` `coeff`	—	—
`coeffAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `coeffAddEquiv` `ofCoeff`	—	—
`coeffEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `coeffEquiv` `coeff`	—	—
`coeffEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `coeffEquiv` `ofCoeff`	—	—
`coeff_add` 📖	mathematical	—	`coeff` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`coeff_eq_zero` 📖	mathematical	—	`coeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	—
`coeff_erase` 📖	mathematical	—	`coeff` `erase` `Finsupp.erase` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coeff_finsuppSum` 📖	mathematical	—	`coeff` `Finsupp.sum` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`map_finsuppSum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`coeff_inj` 📖	mathematical	—	`coeff`	—	`coeff_injective`
`coeff_injective` 📖	mathematical	—	`MonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff`	—	`Equiv.injective`
`coeff_neg` 📖	mathematical	—	`coeff` `Ring.toSemiring` `MonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instNeg` `Ring.toAddCommGroup`	—	—
`coeff_ofCoeff` 📖	mathematical	—	`coeff` `ofCoeff`	—	—
`coeff_smul` 📖	mathematical	—	`coeff` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero` `Finsupp.smulZeroClass`	—	—
`coeff_sub` 📖	mathematical	—	`coeff` `Ring.toSemiring` `MonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instSub` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	—
`coeff_sum` 📖	mathematical	—	`coeff` `Finset.sum` `MonoidAlgebra` `addCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`coeff_update` 📖	mathematical	—	`coeff` `update` `Finsupp.update` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coeff_zero` 📖	mathematical	—	`coeff` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero`	—	—
`curryRingEquiv_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `semiring` `instMul` `Prod.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `curryRingEquiv` `single`	—	`Finsupp.curry_single`
`curryRingEquiv_symm_single` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `semiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `curryRingEquiv` `single`	—	`Finsupp.uncurry_single`
`erase_single` 📖	mathematical	—	`erase` `single` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.erase_single`
`erase_zero` 📖	mathematical	—	`erase` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.erase_of_notMem_support`
`exists` 📖	mathematical	—	`MonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `ofCoeff`	—	`Equiv.exists_congr_left`
`ext` 📖	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike`	—	—	`Finsupp.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike`	—	`ext`
`forall` 📖	mathematical	—	`ofCoeff`	—	`Equiv.forall_congr_left`
`induction_linear` 📖	—	`MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `single`	—	—	`Finsupp.induction_linear`
`induction_on` 📖	—	`DFunLike.coe` `MonoidHom` `MonoidAlgebra` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `MulOne.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—	`Finsupp.induction_linear` `smul_single` `mul_one` `Finsupp.single_zero`
`instIsCancelAdd` 📖	mathematical	—	`IsCancelAdd` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid`	—	—
`intCast_def` 📖	mathematical	—	`MonoidAlgebra` `Ring.toSemiring` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `nonAssocRing` `single` `MulOne.toOne` `MulOneClass.toMulOne` `Ring.toAddGroupWithOne`	—	—
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `MulOpposite`	—	—
`isLocalHom_singleOneRingHom` 📖	mathematical	—	`IsLocalHom` `MonoidAlgebra` `RingHom` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `RingHom.instFunLike` `singleOneRingHom`	—	`single_one_mul_apply` `Finsupp.single_eq_same` `mul_single_one_apply`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `Finsupp.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_def` `Finsupp.sum_apply` `single_apply`
`mul_apply_antidiagonal` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finset.sum_filter` `Finset.sum_product` `Finset.sum_congr` `Finset.ext` `Finset.sum_subset` `Finset.filter_subset` `MulZeroClass.zero_mul` `Finset.filter.congr_simp` `MulZeroClass.mul_zero`
`mul_apply_left` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finsupp.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_apply` `Finset.sum_congr` `Finset.sum_ite_eq'` `MulZeroClass.mul_zero`
`mul_apply_right` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finsupp.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_apply` `Finsupp.sum_comm` `Finset.sum_congr` `Finset.sum_ite_eq'` `MulZeroClass.zero_mul`
`mul_def` 📖	mathematical	—	`MonoidAlgebra` `instMul` `Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mul_single_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_single_apply_aux`
`mul_single_apply_aux` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `Finset.sum_congr` `Finsupp.sum_eq_single` `MulZeroClass.zero_mul`
`mul_single_apply_of_not_exists_mul` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `single`	—	`mul_apply` `Finsupp.sum_single_index` `Finsupp.sum_fun_zero`
`mul_single_one_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `single` `MulOne.toOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_single_apply_aux` `mul_one`
`natCast_def` 📖	mathematical	—	`MonoidAlgebra` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `nonAssocSemiring` `single` `MulOne.toOne` `MulOneClass.toMulOne` `Semiring.toNonAssocSemiring`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup` `Ring.toAddCommGroup`	—	—
`nontrivial` 📖	mathematical	—	`Nontrivial` `MonoidAlgebra`	—	—
`ofCoeff_add` 📖	mathematical	—	`ofCoeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid`	—	—
`ofCoeff_coeff` 📖	mathematical	—	`ofCoeff` `coeff`	—	—
`ofCoeff_eq_zero` 📖	mathematical	—	`ofCoeff` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero`	—	—
`ofCoeff_erase` 📖	mathematical	—	`ofCoeff` `Finsupp.erase` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `erase`	—	—
`ofCoeff_finsuppSum` 📖	mathematical	—	`ofCoeff` `Finsupp.sum` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MonoidAlgebra` `addCommMonoid`	—	`map_finsuppSum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofCoeff_inj` 📖	mathematical	—	`ofCoeff`	—	`ofCoeff_injective`
`ofCoeff_injective` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `ofCoeff`	—	`Equiv.injective`
`ofCoeff_neg` 📖	mathematical	—	`ofCoeff` `Ring.toSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `MonoidAlgebra` `NegZeroClass.toNeg` `addCommGroup`	—	—
`ofCoeff_smul` 📖	mathematical	—	`ofCoeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass`	—	—
`ofCoeff_sub` 📖	mathematical	—	`ofCoeff` `Ring.toSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instSub` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `MonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	—
`ofCoeff_sum` 📖	mathematical	—	`ofCoeff` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MonoidAlgebra` `addCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofCoeff_update` 📖	mathematical	—	`ofCoeff` `Finsupp.update` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `update`	—	—
`ofCoeff_zero` 📖	mathematical	—	`ofCoeff` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	—
`ofMagma_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `MonoidAlgebra` `instMul` `MulHom.funLike` `ofMagma` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`of_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MonoidAlgebra` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`of_commute` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne`	`Commute` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `DFunLike.coe` `MonoidHom` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`single_commute` `Commute.one_left`
`of_injective` 📖	mathematical	—	`MonoidAlgebra` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`NeZero.one` `Finsupp.single_eq_single_iff`
`one_def` 📖	mathematical	—	`MonoidAlgebra` `one` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`prod_single` 📖	mathematical	—	`Finset.prod` `MonoidAlgebra` `CommSemiring.toSemiring` `CommSemiring.toCommMonoid` `commSemiring` `single`	—	`Finset.cons_induction_on` `Finset.prod_cons` `single_mul_single`
`ringHom_ext` 📖	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `single` `MulOne.toOne` `MulOneClass.toMulOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`RingHom.coe_addMonoidHom_injective` `Finsupp.addHom_ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `single_mul_single` `one_mul` `mul_one`
`ringHom_ext'` 📖	—	`RingHom.comp` `MonoidAlgebra` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `singleOneRingHom` `MonoidHom.comp` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHomClass.toMonoidHom` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `of`	—	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ringHom_ext`
`ringHom_ext'_iff` 📖	mathematical	—	`RingHom.comp` `MonoidAlgebra` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `singleOneRingHom` `MonoidHom.comp` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHomClass.toMonoidHom` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `of`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ringHom_ext'`
`singleAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addCommMonoid` `AddMonoidHom.instFunLike` `singleAddHom` `single`	—	—
`singleHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MonoidAlgebra` `MulOneClass.toMulOne` `Prod.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `MonoidHom.instFunLike` `singleHom` `single`	—	—
`singleOneRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MonoidAlgebra` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `RingHom.instFunLike` `singleOneRingHom` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `addCommMonoid` `AddMonoidHom.toZeroHom` `singleAddHom` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`single_add` 📖	mathematical	—	`single` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addCommMonoid`	—	`Finsupp.single_add`
`single_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `single`	—	`Finsupp.single_apply`
`single_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Commute` `MonoidAlgebra` `instMul` `single`	—	`addHom_ext'` `AddMonoidHom.ext` `single_commute_single`
`single_commute_single` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Commute` `MonoidAlgebra` `instMul` `single`	—	`single_mul_single` `Commute.eq`
`single_eq_zero` 📖	mathematical	—	`single` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finsupp.single_eq_zero`
`single_mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`single_mul_apply_aux`
`single_mul_apply_aux` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finsupp.sum_single_index` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `Finset.sum_congr` `Finsupp.sum_eq_single` `MulZeroClass.mul_zero`
`single_mul_apply_of_not_exists_mul` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `single`	—	`mul_apply` `Finsupp.sum_single_index` `Finsupp.sum_fun_zero`
`single_mul_single` 📖	mathematical	—	`MonoidAlgebra` `instMul` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mul_def` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `Finsupp.single_zero` `MulZeroClass.zero_mul`
`single_ne_zero` 📖	—	—	—	—	—
`single_neg` 📖	mathematical	—	`single` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `MonoidAlgebra` `addCommGroup`	—	`Finsupp.single_neg`
`single_one_comm` 📖	mathematical	—	`MonoidAlgebra` `CommSemiring.toSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `single` `MulOne.toOne`	—	`single_commute` `Commute.one_left` `Commute.all`
`single_one_mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `single` `MulOne.toOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`single_mul_apply_aux` `one_mul`
`single_pow` 📖	mathematical	—	`MonoidAlgebra` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `single`	—	`pow_zero` `pow_succ` `single_mul_single`
`single_zero` 📖	mathematical	—	`single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid`	—	`Finsupp.single_zero`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass`	—	—
`smul_single` 📖	mathematical	—	`MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext`
`smul_single'` 📖	mathematical	—	`MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smul_single`
`sum_single` 📖	mathematical	—	`Finsupp.sum` `MonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid` `single`	—	`Finsupp.sum_single`
`sum_single_index` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `single`	—	`Finsupp.sum_single_index`
`uniqueRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `uniqueRingEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finsupp.instFunLike` `Unique.instInhabited`	—	—
`uniqueRingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MonoidAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toAdd` `nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `uniqueRingEquiv` `Equiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Equiv.instEquivLike` `Equiv.symm` `Finsupp.equivFunOnFinite` `uniqueElim`	—	—

(root)

Definitions

Name	Category	Theorems
`AddMonoidAlgebra` 📖	CompOp	407 math math: `AddMonoidAlgebra.sup_support_list_prod_le`, `AddMonoidAlgebra.instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums`, `AddMonoidAlgebra.singleHom_apply`, `AddMonoidAlgebra.mapRangeAlgEquiv_trans`, `AddMonoidAlgebra.instIsCancelAddZeroOfIsCancelAddOfUniqueSums`, `AddMonoidAlgebra.supDegree_sum_lt`, `AddMonoidAlgebra.supportedEquivFinsupp_apply_apply`, `AddMonoidAlgebra.mul_single_apply`, `AddMonoidAlgebra.lift_apply'`, `addMonoidAlgebraEquivDirectSum_apply`, `AddMonoidAlgebra.mapDomainRingEquiv_apply`, `AddMonoidAlgebra.domCongr_comp_lsingle`, `AddMonoidAlgebra.mul_apply`, `Polynomial.ofFinsupp_zero`, `AddMonoidAlgebra.algHom_ext'_iff`, `AddMonoidAlgebra.coeffEquiv_symm_apply`, `AddMonoidAlgebra.liftNC_mul`, `AddMonoidAlgebra.of'_mem_span`, `AddMonoidAlgebra.comapDomain_add`, `AddMonoidAlgebra.liftNCRingHom_single`, `AddMonoidAlgebra.mapDomainNonUnitalRingHom_id`, `Polynomial.toFinsupp_zsmul`, `AddMonoidAlgebra.le_infDegree_add`, `LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply`, `AddMonoidAlgebra.comul_single`, `AddMonoidAlgebra.isScalarTower_self`, `Polynomial.homogenize_smul`, `Polynomial.toFinsupp_pow`, `AddMonoidAlgebra.mapDomainAddEquiv_single`, `AddMonoidAlgebra.zero_divOf`, `AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply`, `AddMonoidAlgebra.of'_divOf`, `AddMonoidAlgebra.domCongr_toAlgHom`, `AddMonoidAlgebra.exists`, `AddMonoidAlgebra.mapDomainAddEquiv_apply`, `AddMonoidAlgebra.Monic.supDegree_mul`, `MvPolynomial.smul_monomial`, `AddMonoidAlgebra.ofCoeff_eq_zero`, `AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val`, `AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right`, `AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums`, `AddMonoidAlgebra.mapDomain_one`, `AddMonoidAlgebra.toRingHom_mapDomainRingEquiv`, `DirectSum.toAddMonoidAlgebra_sub`, `AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap`, `AddMonoidAlgebra.supDegree_add_le`, `AddMonoidAlgebra.instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums`, `AddMonoidAlgebra.mapAlgHom_single`, `AddMonoidAlgebra.divOfHom_apply_apply`, `AddMonoidAlgebra.ofCoeff_neg`, `AddMonoidAlgebra.mapDomainBialgHom_id`, `AddMonoidAlgebra.mapDomainAlgHom_id`, `AddMonoidAlgebra.toRingHom_mapAlgHom`, `AddMonoidAlgebra.uniqueRingEquiv_apply`, `Polynomial.eval₂_ofFinsupp`, `AddMonoidAlgebra.opRingEquiv_symm_single`, `AddMonoidAlgebra.opRingEquiv_symm_apply`, `AddMonoidAlgebra.intCast_def`, `AddMonoidAlgebra.coeff_add`, `Polynomial.ofFinsupp_natCast`, `AddMonoidAlgebra.coeff_sub`, `AddMonoidAlgebra.algebraMap_def`, `AddMonoidAlgebra.mapRingHom_id`, `AddMonoidAlgebra.singleZeroRingHom_apply`, `AddMonoidAlgebra.instIsTorsionFree`, `Polynomial.ofFinsupp_sub`, `AddMonoidAlgebra.ofCoeff_injective`, `AddMonoidAlgebra.counit_single`, `AddMonoidAlgebra.smulCommClass`, `AddMonoidAlgebra.supDegree_mul`, `AddMonoidAlgebra.coeff_sum`, `AddMonoidAlgebra.mapDomainRingHom_comp_algebraMap`, `AddMonoidAlgebra.of'_commute`, `AddMonoidAlgebra.Monic.pow`, `AddMonoidAlgebra.moduleFinite`, `AddMonoidAlgebra.neg_apply`, `BoundedContinuousFunction.mem_charPoly`, `AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom`, `BoundedContinuousFunction.charAlgHom_apply`, `AddMonoidAlgebra.single_commute_single`, `AddMonoidAlgebra.of'_mul_divOf`, `AddMonoidAlgebra.domCongr_refl`, `LieAlgebra.LoopAlgebra.toFinsupp_symm_single`, `AddMonoidAlgebra.decomposeAux_coe`, `AddMonoidAlgebra.lsingle_apply`, `AddMonoidAlgebra.of_apply`, `AddMonoidAlgebra.gradeBy.isInternal`, `Polynomial.ofFinsupp_pow`, `Polynomial.toFinsupp_injective`, `AddMonoidAlgebra.single_add`, `AddMonoidAlgebra.mapAddEquiv_single`, `AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure`, `AddMonoidAlgebra.smul_single`, `DirectSum.toAddMonoidAlgebra_one`, `AddMonoidAlgebra.supDegree_add_eq_right`, `AddMonoidAlgebra.ofCoeff_sub`, `AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left`, `AddMonoidAlgebra.support_mul_single_subset`, `AddMonoidAlgebra.mapRingHom_comp_algebraMap`, `AddMonoidAlgebra.tensorEquiv.invFun_tmul`, `Polynomial.ofFinsupp_algebraMap`, `AddMonoidAlgebra.erase_zero`, `AddMonoidAlgebra.isLocalHom_singleZeroRingHom`, `AddMonoidAlgebra.smul_apply`, `AddMonoidAlgebra.smulCommClass_symm_self`, `AddMonoidAlgebra.le_inf_support_add`, `AddMonoidAlgebra.sup_support_multiset_prod_le`, `AddMonoidAlgebra.commAlgEquiv_single_single`, `AddMonoidAlgebra.ringHom_ext'_iff`, `AddMonoidAlgebra.Monic.mul`, `AddMonoidAlgebra.support_single_mul_subset`, `AddMonoidAlgebra.isScalarTower`, `AddMonoidAlgebra.isLocalHom_algebraMap`, `AddMonoidAlgebra.lift_apply`, `addMonoidAlgebraEquivDirectSum_symm_apply`, `AddMonoidAlgebra.cardinalMk_of_infinite'`, `AddMonoidAlgebra.mem_ideal_span_of'_image`, `Polynomial.toFinsupp_eq_zero`, `Polynomial.ofFinsupp_add`, `AddMonoidAlgebra.leadingCoeff_add_eq_right`, `AddMonoidAlgebra.supDegree_zero`, `AddMonoidAlgebra.mapDomainNonUnitalRingHom_apply`, `AddMonoidAlgebra.leadingCoeff_eq_zero`, `Polynomial.ofFinsupp_eq_one`, `Polynomial.toFinsupp_nsmul`, `AddMonoidAlgebra.toDirectSum_mul`, `AddMonoidAlgebra.domCongr_single`, `AddMonoidAlgebra.leadingCoeff_add_eq_left`, `AddMonoidAlgebra.prod_single`, `AddMonoidAlgebra.mul_def`, `AddMonoidAlgebra.mapDomainBialgHom_apply`, `AddMonoidAlgebra.coe_algebraMap`, `AddMonoidAlgebra.le_inf_support_pow`, `MvPolynomial.coeff_smul`, `AddMonoidAlgebra.supDegree_neg`, `AddMonoidAlgebra.toDirectSum_natCast`, `AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right`, `AddMonoidAlgebra.map_sub`, `AddMonoidAlgebra.comapDomainAddMonoidHom_apply`, `AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero`, `Polynomial.ofFinsupp_one`, `AddMonoidAlgebra.toDirectSum_zero`, `AddMonoidAlgebra.finiteType_of_fg`, `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `AddMonoidAlgebra.apply_add_of_supDegree_le`, `DirectSum.toAddMonoidAlgebra_mul`, `AddMonoidAlgebra.toDirectSum_add`, `AddMonoidAlgebra.coe_add`, `AddMonoidAlgebra.cardinalMk_of_fintype`, `AddMonoidAlgebra.commRingEquiv_single_single`, `AddMonoidAlgebra.leadingCoeff_zero`, `AddMonoidAlgebra.mul_of'_modOf`, `AddMonoidAlgebra.mul_single_zero_apply`, `AddMonoidAlgebra.mapAddEquiv_apply`, `Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp`, `AddMonoidAlgebra.le_inf_support_list_prod`, `AddMonoidAlgebra.finiteType_iff_group_fg`, `AddMonoidAlgebra.coe_mapRingHom`, `DirectSum.toAddMonoidAlgebra_natCast`, `Polynomial.toFinsupp_one`, `AddMonoidAlgebra.symm_mapAddEquiv`, `AddMonoidAlgebra.instIsPushout`, `AddMonoidAlgebra.instIsPushout'`, `AddMonoidAlgebra.toDirectSum_pow`, `AddMonoidAlgebra.coeffLinearEquiv_apply`, `AddMonoidAlgebra.lift_single`, `AddMonoidAlgebra.mapDomainAlgHom_apply`, `Polynomial.toFinsupp_natCast`, `AddMonoidAlgebra.add_divOf`, `MvPolynomial.constantCoeff_smul`, `AddMonoidAlgebra.mapDomainRingHom_comp`, `AddMonoidAlgebra.lift_symm_apply`, `AddMonoidAlgebra.mapDomainRingEquiv_trans`, `AddMonoidAlgebra.faithfulSMul`, `AddMonoidAlgebra.support_mul_single_eq_image`, `AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite'`, `AddMonoidAlgebra.mul_apply_left`, `AddMonoidAlgebra.single_zero_comm`, `AddMonoidAlgebra.cardinalMk_eq_lift_of_fintype`, `AddMonoidAlgebra.GradesBy.decompose_single`, `AddMonoidAlgebra.mapAlgHom_apply`, `AddMonoidAlgebra.toRingHom_mapRingEquiv`, `AddMonoidAlgebra.singleAddHom_apply`, `AddMonoidAlgebra.coe_liftNCAlgHom`, `AddMonoidAlgebra.modOf_add_divOf`, `Polynomial.ofFinsupp_smul`, `AddMonoidAlgebra.supported_eq_span_single`, `AddMonoidAlgebra.monic_one`, `AddMonoidAlgebra.mem_grade_iff'`, `AddMonoidAlgebra.coeff_smul`, `AddMonoidAlgebra.mapRingHom_single`, `AddMonoidAlgebra.natCast_def`, `AddMonoidAlgebra.support_mul`, `AddMonoidAlgebra.lift_of`, `AddMonoidAlgebra.comapDomain_zero`, `Polynomial.toFinsupp_mul`, `DirectSum.toAddMonoidAlgebra_zero`, `AddMonoidAlgebra.nonUnitalAlgHom_ext'_iff`, `LieAlgebra.LoopAlgebra.toFinsupp_single_tmul`, `AddMonoidAlgebra.ofCoeff_zero`, `AddMonoidAlgebra.single_mul_apply`, `AddMonoidAlgebra.supported_eq_map`, `AddMonoidAlgebra.support_one_subset`, `AddMonoidAlgebra.mapRingEquiv_apply`, `AddMonoidAlgebra.single_mul_apply_of_not_exists_add`, `AddMonoidAlgebra.mapDomain_algebraMap`, `AddMonoidAlgebra.single_mem_grade`, `Polynomial.toFinsuppIsoLinear_apply`, `AddMonoidAlgebra.exists_finset_adjoin_eq_top`, `AddMonoidAlgebra.liftMagma_apply_apply`, `AddMonoidAlgebra.coeffAddEquiv_symm_apply`, `LaurentPolynomial.comul_C`, `AddMonoidAlgebra.liftNC_smul`, `AddMonoidAlgebra.mapDomainNonUnitalRingHom_comp`, `AddMonoidAlgebra.liftNC_single`, `AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val`, `AddMonoidAlgebra.toDirectSum_intCast`, `AddMonoidAlgebra.lift_unique'`, `AddMonoidAlgebra.ofCoeff_add`, `AddMonoidAlgebra.opRingEquiv_single`, `AddMonoidAlgebra.smul_single'`, `AddMonoidAlgebra.ofMagma_apply`, `AddMonoidAlgebra.supDegree_leadingCoeff_sum_eq`, `AddMonoidAlgebra.map_add`, `AddMonoidAlgebra.mul_single_apply_aux`, `AddMonoidAlgebra.sup_support_mul_le`, `AddMonoidAlgebra.liftMagma_symm_apply`, `AddMonoidAlgebra.tensorEquiv_tmul`, `AddMonoidAlgebra.gradeBy.gradedMonoid`, `Polynomial.toFinsupp_algebraMap`, `Polynomial.ofFinsupp_neg`, `AddMonoidAlgebra.coeff_eq_zero`, `AddMonoidAlgebra.symm_commAlgEquiv`, `AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd`, `AddMonoidAlgebra.single_mul_single`, `Polynomial.toFinsupp_eq_one`, `AddMonoidAlgebra.erase_single`, `AddMonoidAlgebra.le_infDegree_mul`, `AddMonoidAlgebra.mapDomainAlgHom_comp`, `AddMonoidAlgebra.tensorEquiv_symm_single`, `AddMonoidAlgebra.le_inf_support_mul`, `AddMonoidAlgebra.lift_of'`, `AddMonoidAlgebra.mem_grade_iff`, `AddMonoidAlgebra.curryRingEquiv_symm_single`, `AddMonoidAlgebra.opRingEquiv_apply`, `AddMonoidAlgebra.grade.decompose_single`, `AddMonoidAlgebra.mapDomainRingEquiv_single`, `AddMonoidAlgebra.mem_adjoin_support`, `AddMonoidAlgebra.single_eq_zero`, `Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp`, `LieAlgebra.LoopAlgebra.residuePairing_apply_apply`, `AddMonoidAlgebra.domCongr_support`, `AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left`, `AddMonoidAlgebra.coeffLinearEquiv_symm_apply`, `AddMonoidAlgebra.lhom_ext'_iff`, `AddMonoidAlgebra.Monic.supDegree_pow`, `AddMonoidAlgebra.lift_mapRingHom_algebraMap`, `AddMonoidAlgebra.single_zero`, `MvPolynomial.support_smul_eq`, `AddMonoidAlgebra.curryAlgEquiv_symm_single`, `AddMonoidAlgebra.domCongr_symm`, `AddMonoidAlgebra.supDegree_sub_lt_of_leadingCoeff_eq`, `Polynomial.toFinsuppIso_apply`, `AddMonoidAlgebra.uniqueRingEquiv_symm_apply`, `AddMonoidAlgebra.leadingCoeff_mul`, `MonoidAlgebra.Submodule.instIsSemisimpleRingAddMonoidAlgebra`, `AddMonoidAlgebra.mapDomain_mul`, `AddMonoidAlgebra.coeff_finsuppSum`, `AddMonoidAlgebra.algHom_ext_iff`, `Polynomial.toFinsupp_sum`, `AddMonoidAlgebra.supported_mono`, `AddMonoidAlgebra.sup_support_pow_le`, `AddMonoidAlgebra.symm_mapDomainRingEquiv`, `DirectSum.toAddMonoidAlgebra_intCast`, `BoundedContinuousFunction.star_mem_range_charAlgHom`, `AddMonoidAlgebra.supDegree_add_eq_left`, `AddMonoidAlgebra.basis_apply`, `DirectSum.toAddMonoidAlgebra_add`, `AddMonoidAlgebra.grade.isInternal`, `Polynomial.toFinsupp_add`, `Polynomial.toFinsupp_neg`, `Polynomial.toFinsupp_smul`, `AddMonoidAlgebra.mapDomain_zero`, `AddMonoidAlgebra.supDegree_mul_le`, `AddMonoidAlgebra.toDirectSum_sub`, `AddMonoidAlgebra.coeffAddEquiv_apply`, `AddMonoidAlgebra.divOf_add_modOf`, `Polynomial.ofFinsupp_mul`, `Polynomial.exists_iff_exists_finsupp`, `AddMonoidAlgebra.coeff_injective`, `AddMonoidAlgebra.mapDomainBialgHom_comp`, `AddMonoidAlgebra.liftNC_one`, `AddMonoidAlgebra.scalarTensorEquiv_symm_single`, `AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply`, `AddMonoidAlgebra.of_injective`, `AddMonoidAlgebra.sup_support_add_le`, `AddMonoidAlgebra.supDegree_sub_le`, `Polynomial.toFinsuppIsoAlg_apply`, `AddMonoidAlgebra.finiteType_iff_fg`, `AddMonoidAlgebra.ofCoeff_sum`, `AddMonoidAlgebra.support_single_mul`, `AddMonoidAlgebra.instIsCocomm`, `Polynomial.toFinsupp_sub`, `AddMonoidAlgebra.support_single_mul_eq_image`, `AddMonoidAlgebra.single_pow`, `AddMonoidAlgebra.instFree`, `AddMonoidAlgebra.single_zero_mul_apply`, `AddMonoidAlgebra.map_one`, `AddMonoidAlgebra.toDirectSum_neg`, `AddMonoidAlgebra.domCongr_apply`, `AddMonoidAlgebra.mapAddEquiv_trans`, `LaurentPolynomial.comul_C_mul_T`, `Polynomial.ofFinsupp_zsmul`, `AddMonoidAlgebra.map_neg`, `AddMonoidAlgebra.single_neg`, `AddMonoidAlgebra.support_gen_of_gen`, `AddMonoidAlgebra.single_mul_apply_aux`, `AddMonoidAlgebra.mem_supported'`, `AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite`, `AddMonoidAlgebra.mem_span_support'`, `Polynomial.toFinsuppIso_symm_apply`, `LaurentPolynomial.smul_eq_C_mul`, `AddMonoidAlgebra.decomposeAux_single`, `AddMonoidAlgebra.ofCoeff_finsuppSum`, `AddMonoidAlgebra.mapDomainAddEquiv_trans`, `MvPolynomial.totalDegree_smul_le`, `AddMonoidAlgebra.nontrivial`, `AddMonoidAlgebra.sup_support_finset_prod_le`, `AddMonoidAlgebra.curryRingEquiv_single`, `AddMonoidAlgebra.addHom_ext'_iff`, `addMonoidAlgebraAddEquivDirectSum_symm_apply`, `DirectSum.toAddMonoidAlgebra_pow`, `AddMonoidAlgebra.antipode_single`, `AddMonoidAlgebra.decomposeAux_eq_decompose`, `Polynomial.ofFinsupp_eq_zero`, `addMonoidAlgebraRingEquivDirectSum_apply`, `AddMonoidAlgebra.symm_mapAlgEquiv`, `AddMonoidAlgebra.mapDomain_add`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`, `AddMonoidAlgebra.lift_unique`, `AddMonoidAlgebra.lift_def`, `AddMonoidAlgebra.instIsCancelAdd`, `AddMonoidAlgebra.ofCoeff_smul`, `AddMonoidAlgebra.singleZeroAlgHom_apply`, `AddMonoidAlgebra.coeff_zero`, `AddMonoidAlgebra.mapDomainRingHom_id`, `addMonoidAlgebraAddEquivDirectSum_apply`, `AddMonoidAlgebra.le_inf_support_finset_prod`, `AddMonoidAlgebra.of'_mul_modOf`, `AddMonoidAlgebra.scalarTensorEquiv_tmul`, `DirectSum.toAddMonoidAlgebra_neg`, `LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe`, `AddMonoidAlgebra.le_inf_support_multiset_prod`, `AddMonoidAlgebra.distribMulActionHom_ext'_iff`, `Polynomial.ofFinsupp_sum`, `AddMonoidAlgebra.of'_modOf`, `AddMonoidAlgebra.symm_mapRingEquiv`, `Polynomial.toFinsupp_intCast`, `AddMonoidAlgebra.sum_single`, `AddMonoidAlgebra.mapRingHom_apply`, `AddMonoidAlgebra.symm_commRingEquiv`, `AddMonoidAlgebra.map_sum`, `AddMonoidAlgebra.single_mem_gradeBy`, `addMonoidAlgebraAlgEquivDirectSum_apply`, `AddMonoidAlgebra.single_commute`, `AddMonoidAlgebra.coeff_neg`, `AddMonoidAlgebra.grade.gradedMonoid`, `AddMonoidAlgebra.support_gen_of_gen'`, `AddMonoidAlgebra.symm_mapDomainAddEquiv`, `AddMonoidAlgebra.of'_eq_of`, `AddMonoidAlgebra.mapRingHom_comp`, `MvPolynomial.support_smul`, `AddMonoidAlgebra.isLocalHom_singleZeroAlgHom`, `AddMonoidAlgebra.isCentralScalar`, `AddMonoidAlgebra.coeffEquiv_apply`, `AddMonoidAlgebra.supDegree_prod_le`, `AddMonoidAlgebra.mul_apply_right`, `AddMonoidAlgebra.cardinalMk_of_infinite`, `Polynomial.toFinsupp_zero`, `AddMonoidAlgebra.curryAlgEquiv_single`, `Polynomial.ofFinsupp_nsmul`, `AddMonoidAlgebra.map_zero`, `AddMonoidAlgebra.smulCommClass_self`, `AddMonoidAlgebra.mem_gradeBy_iff`, `AddMonoidAlgebra.mul_single_apply_of_not_exists_add`, `AddMonoidAlgebra.toDirectSum_one`, `AddMonoidAlgebra.one_def`, `AddMonoidAlgebra.mapDomain_sum`, `AddMonoidAlgebra.mem_span_support`, `AddMonoidAlgebra.support_mul_single`, `AddMonoidAlgebra.mapDomain_injective`, `AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure`, `AddMonoidAlgebra.mapAlgEquiv_apply`, `AddMonoidAlgebra.mapRingEquiv_trans`, `Polynomial.ofFinsupp_intCast`, `AddMonoidAlgebra.map_mul`, `AddMonoidAlgebra.mapDomainRingHom_apply`, `AddMonoidAlgebra.mapRingEquiv_single`, `AddMonoidAlgebra.mul_apply_antidiagonal`, `AddMonoidAlgebra.support_one`, `AddMonoidAlgebra.instIsDomainOfIsCancelAddOfUniqueSums`, `AddMonoidAlgebra.mem_supported`, `AddMonoidAlgebra.apply_supDegree_add_supDegree`, `AddMonoidAlgebra.vaddAssocClass_addMonoidAlgebra`, `AddMonoidAlgebra.supDegree_sum_le`, `AddMonoidAlgebra.mapRingHom_comp_mapDomainRingHom`, `AddMonoidAlgebra.mul_of'_divOf`

---

← Back to Index