MvPowerSeries.restrictedProductEquivPolynomialReduction |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/InverseLimit.lean, line 117 |
|
MvPolynomial.adicCompletionMap |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/CompletionMap.lean, line 92 |
|
MvPolynomial.adicPolynomialLevelEquiv_evalₐ_adicCompletionMap |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/CompletionMap.lean, line 171 |
|
MvPolynomial.adicCompletionMap_comp_completedCoefficient |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/CompletionMap.lean, line 237 |
|
MvPowerSeries.completedRestrictedRename |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/CompletedRename.lean, line 230 |
|
MvPowerSeries.completedRestrictedCoeffMap |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 76 |
|
MvPowerSeries.completedRestrictedMap |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 312 |
|
MvPowerSeries.coeff_completedRestrictedMap_eval |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 350 |
|
MvPowerSeries.completedRestrictedMap_comp |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 409 |
|
MvPowerSeries.completedRestrictedMap_comp_algebraMap |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 508 |
|
MvPowerSeries.ker_polynomialReduction_le_comap_completedRestrictedMap |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 566 |
|
MvPolynomial.adicCompletionEquiv_naturality |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 687 |
|
MvPolynomial.adicCompletionEquiv_symm_naturality |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Naturality.lean, line 816 |
|
MvPowerSeries.IsAdicallyRestricted.mono |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/IdealChange.lean, line 29 |
|
MvPowerSeries.restrictAlongIdeal |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/IdealChange.lean, line 45 |
|
MvPowerSeries.restrictAlongIdeal_trans |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/IdealChange.lean, line 70 |
|
MvPowerSeries.reductionAtLargerIdeal |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/IdealChange.lean, line 88 |
|
MvPowerSeries.reductionAtLargerIdeal_surjective |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/IdealChange.lean, line 113 |
|
MvPowerSeries.restrictedResidueHom |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/ValuationResidue.lean, line 33 |
|
MvPowerSeries.restrictedResidueHom_apply |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/ValuationResidue.lean, line 64 |
|
MvPowerSeries.restrictedRenameEquiv |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Rename.lean, line 46 |
|
MvPowerSeries.restrictedFirstRegroup |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableRegrouping.lean, line 76 |
|
MvPowerSeries.polynomialRestrictedFirst |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableRegrouping.lean, line 199 |
|
MvPowerSeries.restrictedFirst_actual_support_iff |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableRegrouping.lean, line 244 |
|
MvPowerSeries.restrictedFinSuccEquiv |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableRegrouping/Fin.lean, line 28 |
|
MvPowerSeries.restrictedFinFirst_actual_support_iff |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableRegrouping/Fin.lean, line 140 |
|
MvPowerSeries.isUnit_adicallyRestricted_iff_adicReduction_one |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/UnitDetection.lean, line 28 |
|
MvPowerSeries.isUnit_adicallyRestricted_iff_coeff_mod_ideal |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/UnitDetection.lean, line 65 |
|
MvPowerSeries.isUnit_iff_quotient_of_isAdicComplete |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/UnitDetection.lean, line 77 |
|
MvPowerSeries.isUnit_adicallyRestricted_iff_coeff_radical |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/UnitDetection.lean, line 85 |
|
MvPowerSeries.isAdicallyRestricted_iff_degree_cutoff |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/DegreeDecay.lean, line 38 |
|
MvPowerSeries.exists_restricted_fg_decomposition |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FinitelyGeneratedKernel.lean, line 30 |
|
MvPowerSeries.ker_adicReduction_fg |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FinitelyGeneratedKernel.lean, line 107 |
|
MvPowerSeries.adicallyRestrictedAlgebra |
instance |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 30 |
|
MvPowerSeries.algebraMap_adicallyRestricted_coe |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 35 |
|
MvPowerSeries.coe_smul_adicallyRestricted |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 42 |
|
MvPowerSeries.coeff_smul_adicallyRestricted |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 49 |
|
MvPowerSeries.algebraAdicReduction |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 56 |
|
MvPowerSeries.linearAdicReduction |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 63 |
|
MvPowerSeries.linearAdicReduction_apply |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 68 |
|
MvPowerSeries.coeff_linearAdicReduction |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 74 |
|
MvPowerSeries.linearAdicReduction_surjective |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 80 |
|
MvPowerSeries.principalAdicConstant_mul_eq_smul |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 85 |
|
MvPowerSeries.ker_linearAdicReduction_principal |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 95 |
|
MvPowerSeries.principalLinearQuotientEquiv |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 125 |
|
MvPowerSeries.principalLinearQuotientEquiv_mk |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 137 |
|
MvPowerSeries.intLinearAdicReduction |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 144 |
|
MvPowerSeries.intLinearAdicReduction_apply |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 149 |
|
MvPowerSeries.coeff_intLinearAdicReduction |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 155 |
|
MvPowerSeries.intLinearAdicReduction_surjective |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 161 |
|
MvPowerSeries.principalAdicConstant_mul_eq_int_smul |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 166 |
|
MvPowerSeries.ker_intLinearAdicReduction_principal |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 179 |
|
MvPowerSeries.principalIntLinearQuotientEquiv |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 209 |
|
MvPowerSeries.principalIntLinearQuotientEquiv_mk |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearQuotient.lean, line 221 |
|
MvPowerSeries.polynomialLinearMapMod |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 28 |
|
MvPowerSeries.polynomialLinearMapMod_map |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 45 |
|
MvPowerSeries.polynomialLinearMapMod_factorPow |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 60 |
|
MvPowerSeries.restrictedLinearExtension |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 163 |
|
MvPowerSeries.adicReduction_restrictedLinearExtension |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 186 |
|
MvPowerSeries.restrictedLinearExtension_polynomial |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 195 |
|
MvPowerSeries.restrictedLinearExtension_preserves_ker |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 207 |
|
MvPowerSeries.restrictedLinearExtension_unique |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LinearExtension.lean, line 218 |
|
MvPowerSeries.coeff_mul_mem_ideal_mul_ideal |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/KernelFiltration.lean, line 44 |
|
MvPowerSeries.adicReduction_mul_eq_zero |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/KernelFiltration.lean, line 54 |
|
MvPowerSeries.adicReduction_sum_mul_eq_zero |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/KernelFiltration.lean, line 75 |
|
MvPowerSeries.adicReduction_sum_mul_eq_zero_succ |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/KernelFiltration.lean, line 85 |
|
MvPowerSeries.IsAdicallyRestricted.exists_span_range_eq_span_coeff |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Content.lean, line 59 |
|
MvPowerSeries.IsAdicallyRestricted.exists_selected_coeff_factor |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/SelectedFactor.lean, line 68 |
|
MonomialOrder.restrictedLeadingTermIdeal |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LeadingTerm.lean, line 346 |
|
MvPowerSeries.exists_common_monic_parameter |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/MonicParameter.lean, line 80 |
|
MonomialOrder.restrictedDivisionRemainder |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/PolynomialDivision.lean, line 30 |
|
MvPowerSeries.restrictedGeometricInverse |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/RestrictedGeometricInverse.lean, line 176 |
|
MonomialOrder.restrictedPerturbedDivisionRemainder |
def |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/PerturbedDivision.lean, line 79 |
|
MonomialOrder.exists_restricted_monic_division |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/MonicDivision.lean, line 30 |
|
MvPowerSeries.isAdicallyRestricted_iff_of_cofinal |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/Cofinal.lean, line 26 |
|
isHausdorff_iff_of_cofinal |
theorem |
FormalPowerSeries/AdicCompletion/Cofinal.lean, line 38 |
|
isPrecomplete_iff_of_cofinal |
theorem |
FormalPowerSeries/AdicCompletion/Cofinal.lean, line 51 |
|
isAdicComplete_iff_of_cofinal |
theorem |
FormalPowerSeries/AdicCompletion/Cofinal.lean, line 80 |
|
MonomialOrder.exists_restricted_primitive_division |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/ValuationNormalizedDivision.lean, line 35 |
|
MonomialOrder.ideal_eq_span_of_primitive_standardBasis |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/PrimitiveStandardBasis.lean, line 93 |
|
MonomialOrder.restrictedLeadingExponent_mul_of_ne_zero |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/LeadingTerm/Product.lean, line 34 |
|
MonomialOrder.restricted_singleton_division_unique |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/SingletonDivision.lean, line 35 |
|
MonomialOrder.existsUnique_restricted_primitive_singleton_division |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/SingletonDivision.lean, line 86 |
|
MvPowerSeries.restrictedLeadingExponent_lex_eq_cons_of_scalar_top |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableDivision.lean, line 31 |
|
MvPowerSeries.existsUnique_firstVariable_division_of_leadingExponent |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableDivision.lean, line 50 |
|
MvPowerSeries.existsUnique_firstVariable_division_of_scalar_top |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableDivision.lean, line 114 |
|
MvPowerSeries.exists_firstVariable_monomial_division_of_scalar_top |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableDivision.lean, line 136 |
|
MvPowerSeries.isUnit_of_isUnit_restrictedResidueHom |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/UnitDetection/Residue.lean, line 39 |
|
MvPowerSeries.isUnit_of_isUnit_restrictedResidue |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/UnitDetection/Residue.lean, line 72 |
|
MvPowerSeries.finSuccEquiv_restrictedResidueHom_polynomialRestrictedFinFirst |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableUnit.lean, line 38 |
|
MvPowerSeries.restrictedResidueHom_quotient_of_restrictedFinFirst_division |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableUnit.lean, line 117 |
|
MvPowerSeries.isUnit_quotient_of_restrictedFinFirst_divisionHom |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableUnit.lean, line 181 |
|
MvPowerSeries.restrictedResidue_quotient_of_restrictedFinFirst_division |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableUnit.lean, line 210 |
|
MvPowerSeries.isUnit_quotient_of_restrictedFinFirst_division |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariableUnit.lean, line 234 |
|
MvPowerSeries.existsUnique_firstVariable_preparation_of_scalar_top_of_primitive |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariablePreparation.lean, line 32 |
|
MvPowerSeries.existsUnique_firstVariable_preparation_of_scalar_top |
theorem |
FormalPowerSeries/MvPowerSeries/IdealAdicRestricted/FirstVariablePreparation.lean, line 102 |
|