Defs

📁 Source: Mathlib/Algebra/Group/Nat/Defs.lean

Statistics

Metric	Count
Definitions instAddCancelCommMonoid, instAddCommMonoid, instAddCommSemigroup, instAddMonoid, instAddSemigroup, instCommMonoid, instCommSemigroup, instMonoid, instMulOneClass, instOne, instSemigroup	11
Theorems instIsAddTorsionFree, instIsMulTorsionFree, nsmul_eq_mul	3
Total	14

Nat

Definitions

Name	Category	Theorems
instAddCancelCommMonoid 📖	CompOp	723 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, CategoryTheory.InjectiveResolution.injective, CategoryTheory.InjectiveResolution.Hom.hom'_f, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, CochainComplex.augment_d_succ_succ, AlgebraicTopology.DoldKan.P_f_0_eq, ChainComplex.truncate_map_f, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, groupCohomology.toCocycles_comp_isoCocycles₁_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, ComplexShape.instHasNoLoopNatDown, SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, AlgebraicTopology.NormalizedMooreComplex.obj_d, groupCohomology.inhomogeneousCochains.d_def, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, groupCohomology.cocyclesIso₀_hom_comp_f, CategoryTheory.InjectiveResolution.ι'_f_zero, instIsAddTorsionFree, CategoryTheory.ProjectiveResolution.quasiIso, CochainComplex.augmentTruncate_inv_f_zero, groupCohomology.eq_d₀₁_comp_inv, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, ChainComplex.mkHom_f_0, CochainComplex.quasiIso_truncLEMap_iff, groupCohomology.eq_d₁₂_comp_inv, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, AlgebraicTopology.DoldKan.identity_N₂, groupHomology.eq_d₃₂_comp_inv, Homotopy.mkInductiveAux₃, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE, CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, groupHomology.chainsMap_id, SimplicialObject.Splitting.PInfty_comp_πSummand_id, Rep.barComplex.d_def, CategoryTheory.InjectiveResolution.self_ι, Finsupp.mapDomain_comapDomain_nat_add_one, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, ChainComplex.mk'_X_0, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, CochainComplex.mk'_X_0, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Abelian.LeftResolution.chainComplexMap_id, ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE, AlgebraicTopology.DoldKan.PInfty_idem, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, groupHomology.comp_d₂₁_eq, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, CochainComplex.ConnectData.d_ofNat, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, CochainComplex.augment_X_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, AlgebraicTopology.DoldKan.QInfty_idem, ChainComplex.isoHomologyι₀_inv_naturality_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, CochainComplex.truncate_obj_X, CochainComplex.ConnectData.map_comp_map, groupCohomology.cochainsMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, ChainComplex.mk_X_2, groupCohomology.comp_d₁₂_eq, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.InjectiveResolution.of_def, CategoryTheory.Preadditive.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.self_π, CategoryTheory.ProjectiveResolution.cochainComplex_d, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupCohomology.dArrowIso₀₁_inv_right, CochainComplex.ConnectData.d_zero_one, groupCohomology.eq_d₂₃_comp_inv_assoc, groupCohomology.eq_d₂₃_comp_inv_apply, CategoryTheory.InjectiveResolution.complex_d_comp, groupCohomology.eq_d₁₂_comp_inv_apply, ComplexShape.Embedding.embeddingUpInt_areComplementary, Rep.standardComplex.d_eq, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, Homotopy.prevD_succ_cochainComplex, CategoryTheory.ProjectiveResolution.sub_extMk, CategoryTheory.Functor.mapProjectiveResolution_π, CategoryTheory.instIsIsoToRightDerivedZero', groupHomology.chainsMap_id_f_map_mono, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, CochainComplex.fromSingle₀Equiv_apply_coe, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, Finset.range_add, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, groupHomology.chainsMap_f_3_comp_chainsIso₃, ChainComplex.single₀ObjXSelf, groupHomology.eq_d₂₁_comp_inv, AlgebraicTopology.DoldKan.QInfty_idem_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc, groupCohomology.dArrowIso₀₁_hom_right, AlgebraicTopology.AlternatingFaceMapComplex.map_f, groupCohomology.toCocycles_comp_isoCocycles₂_hom, AlgebraicTopology.DoldKan.QInfty_f, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, ChainComplex.toSingle₀Equiv_apply_coe, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, CategoryTheory.Functor.mapProjectiveResolution_complex, AlgebraicTopology.alternatingFaceMapComplex_map_f, SimplicialObject.Splitting.nondegComplex_d, AlgebraicTopology.DoldKan.P_f_idem_assoc, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, Rep.standardComplex.εToSingle₀_comp_eq, ChainComplex.mkHom_f_1, AlgebraicTopology.DoldKan.Γ₀'_obj, groupHomology.inhomogeneousChains.d_def, ChainComplex.exactAt_succ_single_obj, ChainComplex.mk_d_1_0, CategoryTheory.Idempotents.DoldKan.hε, groupCohomology.comp_d₂₃_eq, ChainComplex.truncateAugment_inv_f, CategoryTheory.InjectiveResolution.extMk_surjective, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, AlgebraicTopology.DoldKan.QInfty_f_0, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CochainComplex.ConnectData.d_negSucc, CategoryTheory.InjectiveResolution.ι_f_succ, ChainComplex.next_nat_succ, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.ProjectiveResolution.extMk_comp_mk₀, Homotopy.dNext_zero_chainComplex, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, groupHomology.chainsMap_f_single, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc, ComplexShape.embeddingUpNat_f, Homotopy.prevD_chainComplex, groupCohomology.cochainsMap_f_map_epi, groupCohomology.comp_d₀₁_eq, AlgebraicTopology.DoldKan.map_Hσ, CategoryTheory.InjectiveResolution.add_extMk, ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, groupHomology.toCycles_comp_isoCycles₁_hom_apply, CochainComplex.mk_d_2_0, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, prevD_nat, CategoryTheory.InjectiveResolution.extMk_zero, AlgebraicTopology.DoldKan.Γ₀_obj_map, CochainComplex.isoHomologyπ₀_inv_naturality, groupCohomology.cochainsMap_zero, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, groupCohomology.dArrowIso₀₁_inv_left, CochainComplex.exactAt_succ_single_obj, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, groupHomology.map_chainsFunctor_shortExact, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, CochainComplex.augment_X_succ, CochainComplex.mk'_X_1, CategoryTheory.ProjectiveResolution.extMk_hom, groupHomology.eq_d₃₂_comp_inv_apply, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, CochainComplex.single₀_map_f_zero, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, ChainComplex.augmentTruncate_inv_f_succ, groupCohomology.cochainsMap_id_comp, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, ChainComplex.augment_X_succ, CochainComplex.ConnectData.map_f, ChainComplex.quasiIsoAt₀_iff, groupCohomology.cochainsMap_comp_assoc, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, groupHomology.chainsMap_f_map_epi, CochainComplex.ConnectData.d_sub_two_sub_one, groupHomology.isoShortComplexH1_hom, CochainComplex.augment_d_zero_one, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, groupCohomology.isoCocycles₂_hom_comp_i, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, CategoryTheory.ProjectiveResolution.of_def, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CategoryTheory.ProjectiveResolution.π_f_succ, groupCohomology.dArrowIso₀₁_hom_left, AlgebraicTopology.inclusionOfMooreComplex_app, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, AlgebraicTopology.DoldKan.P_f_idem, groupCohomology.eq_d₀₁_comp_inv_apply, AlgebraicTopology.DoldKan.PInfty_idem_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, CochainComplex.ConnectData.restrictionLEIso_inv_f, CategoryTheory.ProjectiveResolution.add_extMk, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupHomology.chainsFunctor_obj, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, CategoryTheory.ProjectiveResolution.Hom.hom'_f, CochainComplex.quasiIso_truncGEMap_iff, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, ChainComplex.isIso_descOpcycles_iff, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, SimplicialObject.Splitting.nondegComplex_X, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, ComplexShape.instIsRelIffNatIntEmbeddingDownNat, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy, groupHomology.d₁₀ArrowIso_inv_right, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', CategoryTheory.InjectiveResolution.extMk_eq_zero_iff, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, ChainComplex.mk_X_0, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, groupHomology.chainsMap_id_f_map_epi, CochainComplex.truncateAugment_inv_f, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, AlgebraicTopology.DoldKan.map_PInfty_f, AlgebraicTopology.DoldKan.P_succ, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, CochainComplex.ConnectData.X_zero, groupCohomology.cochainsMap_id_f_map_mono, groupHomology.chainsMap_id_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, SimplicialObject.Split.nondegComplexFunctor_map_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, groupHomology.isoCycles₂_hom_comp_i_apply, AlgebraicTopology.DoldKan.Hσ_eq_zero, CochainComplex.ConnectData.d₀_comp, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, AlgebraicTopology.normalizedMooreComplex_objD, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, CategoryTheory.InjectiveResolution.self_cocomplex, CategoryTheory.ProjectiveResolution.lift_commutes_zero, groupCohomology.isoCocycles₁_inv_comp_iCocycles, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, groupHomology.eq_d₂₁_comp_inv_assoc, ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp, groupHomology.cyclesIso₀_inv_comp_iCycles, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, CochainComplex.mkHom_f_succ_succ, AlgebraicTopology.DoldKan.Q_idem_assoc, AlgebraicTopology.DoldKan.PInfty_f, ChainComplex.isoHomologyι₀_inv_naturality, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, AlgebraicTopology.DoldKan.Q_f_0_eq, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, CochainComplex.ConnectData.X_ofNat, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, AlgebraicTopology.DoldKan.QInfty_f_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, CochainComplex.instQuasiIsoIntιTruncLEOfIsLE, ChainComplex.next_nat_zero, ComplexShape.boundaryGE_embeddingUpIntGE_iff, CochainComplex.truncate_map_f, ChainComplex.augmentTruncate_hom_f_succ, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, CochainComplex.prev_nat_succ, CategoryTheory.ProjectiveResolution.exact_succ, CategoryTheory.ProjectiveResolution.π'_f_zero, CochainComplex.isIso_liftCycles_iff, AlgebraicTopology.DoldKan.P_f_naturality_assoc, CategoryTheory.InjectiveResolution.desc_commutes, CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp, AlgebraicTopology.DoldKan.map_P, Homotopy.mkCoinductiveAux₂_add_one, Finset.disjoint_range_addLeftEmbedding, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, groupHomology.chainsMap_f_map_mono, CategoryTheory.InjectiveResolution.desc_commutes_assoc, groupHomology.eq_d₁₀_comp_inv, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, groupHomology.isoShortComplexH1_inv, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, groupHomology.eq_d₁₀_comp_inv_assoc, CochainComplex.ConnectData.restrictionLEIso_hom_f, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, AlgebraicTopology.DoldKan.P_idem, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, groupCohomology.cochainsMap_f, CategoryTheory.ProjectiveResolution.complex_d_succ_comp, AlgebraicTopology.DoldKan.Γ₀.map_app, Homotopy.dNext_succ_chainComplex, Homotopy.mkCoinductiveAux₂_zero, groupHomology.chainsMap_comp, AlgebraicTopology.DoldKan.natTransP_app, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, SimplicialObject.Split.nondegComplexFunctor_obj, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, AlgebraicTopology.DoldKan.N₁_obj_X, AlgebraicTopology.map_alternatingFaceMapComplex, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc, groupCohomology.cocyclesMk₁_eq, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.quasiIso_πTruncGE_iff, CategoryTheory.ProjectiveResolution.hasHomology, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_obj, AlgebraicTopology.DoldKan.Q_is_eventually_constant, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, CategoryTheory.ProjectiveResolution.extMk_zero, groupHomology.toCycles_comp_isoCycles₂_hom_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, ChainComplex.mk'_d, CategoryTheory.ProjectiveResolution.self_complex, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.InjectiveResolution.sub_extMk, groupHomology.eq_d₃₂_comp_inv_assoc, ChainComplex.truncateAugment_hom_f, AlgebraicTopology.DoldKan.Q_succ, AlgebraicTopology.DoldKan.natTransPInfty_f_app, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, Rep.standardComplex.d_comp_ε, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.Functor.leftDerived_map_eq, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, CochainComplex.ConnectData.X_negOne, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, CategoryTheory.Abelian.DoldKan.equivalence_inverse, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, groupHomology.isoShortComplexH2_hom, ChainComplex.augmentTruncate_hom_f_zero, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, CochainComplex.ConnectData.X_negSucc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, ComplexShape.instIsRelIffNatIntEmbeddingUpNat, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff, AlgebraicTopology.DoldKan.hσ'_eq, ChainComplex.toSingle₀Equiv_symm_apply_f_zero, groupHomology.chainsMap_f_2_comp_chainsIso₂, AlgebraicTopology.DoldKan.MorphComponents.id_a, groupHomology.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, ChainComplex.instHasHomologyNatObjAlternatingConst, CategoryTheory.InjectiveResolution.mk₀_comp_extMk, AlgebraicTopology.DoldKan.PInfty_f_0, groupCohomology.eq_d₂₃_comp_inv, groupCohomology.cochainsMap_f_map_mono, Homotopy.mkCoinductiveAux₃, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, CategoryTheory.InjectiveResolution.extMk_hom, groupCohomology.isoShortComplexH1_hom, CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor, AlgebraicTopology.DoldKan.PInfty_f_naturality, CategoryTheory.InjectiveResolution.cochainComplex_d_assoc, AlgebraicTopology.DoldKan.hσ'_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles, CochainComplex.quasiIso_ιTruncLE_iff, ChainComplex.isIso_homologyι₀, ChainComplex.truncate_obj_d, inhomogeneousCochains.d_eq, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, CochainComplex.quasiIsoAt₀_iff, Rep.FiniteCyclicGroup.resolution_complex, groupHomology.chainsFunctor_map, groupCohomology.cocyclesMk₂_eq, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, ComplexShape.embeddingUpIntLE_f, groupCohomology.cochainsMap_id_f_map_epi, groupHomology.chainsMap_f_hom, CochainComplex.ConnectData.restrictionGEIso_inv_f, AlgebraicTopology.DoldKan.P_is_eventually_constant, AlgebraicTopology.DoldKan.map_Q, CategoryTheory.ProjectiveResolution.extMk_surjective, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, CochainComplex.ConnectData.map_id, AlgebraicTopology.DoldKan.PInfty_f_idem, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, AlgebraicTopology.DoldKan.N₂_obj_p_f, groupHomology.cyclesMk₁_eq, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc, AlgebraicTopology.DoldKan.σ_comp_PInfty, CochainComplex.mkHom_f_1, ComplexShape.embeddingDownNat_f, groupCohomology.isoCocycles₁_hom_comp_i, CochainComplex.augmentTruncate_inv_f_succ, AlgebraicTopology.NormalizedMooreComplex.obj_X, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, AlgebraicTopology.DoldKan.N₂_obj_X_X, CategoryTheory.Functor.rightDerived_map_eq, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, Rep.standardComplex.instQuasiIsoNatεToSingle₀, CochainComplex.mk_X_2, Rep.standardComplex.x_projective, Homotopy.prevD_zero_cochainComplex, CochainComplex.mkHom_f_0, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, CochainComplex.ConnectData.d₀_comp_assoc, ChainComplex.fromSingle₀Equiv_apply, Finset.range_add_eq_union, TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor, CategoryTheory.InjectiveResolution.desc_commutes_zero, Rep.FiniteCyclicGroup.resolution_quasiIso, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, AlgebraicTopology.DoldKan.P_zero, CochainComplex.augmentTruncate_hom_f_succ, groupCohomology.cochainsMap_f_hom, Rep.standardComplex.d_apply, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, ChainComplex.chainComplex_d_succ_succ_zero, CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, CochainComplex.ConnectData.homologyMap_map_of_eq_succ, AlgebraicTopology.alternatingCofaceMapComplex_map, CategoryTheory.Idempotents.DoldKan.equivalence_functor, AlgebraicTopology.DoldKan.N₂_obj_X_d, groupHomology.isoCycles₁_hom_comp_i_assoc, CategoryTheory.Abelian.DoldKan.equivalence_functor, ChainComplex.augment_d_succ_succ, groupCohomology.isoShortComplexH2_hom, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CategoryTheory.ProjectiveResolution.exact₀, CategoryTheory.InjectiveResolution.hasHomology, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CochainComplex.fromSingle₀Equiv_symm_apply_f_zero, CochainComplex.ConnectData.comp_d₀, ChainComplex.augmentTruncate_inv_f_zero, CochainComplex.truncateAugment_hom_f, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, ComplexShape.instIsTruncLENatIntEmbeddingDownNat, CategoryTheory.InjectiveResolution.neg_extMk, CategoryTheory.Idempotents.DoldKan.Γ_map_app, CategoryTheory.ProjectiveResolution.projective, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, ChainComplex.alternatingConst_exactAt, CochainComplex.toSingle₀Equiv_apply, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.chainsMap_zero, groupHomology.isoShortComplexH2_inv, CochainComplex.cochainComplex_d_succ_succ_zero, groupHomology.toCycles_comp_isoCycles₁_hom, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, groupCohomology.iCocycles_mk, AlgebraicTopology.DoldKan.QInfty_f_idem, groupHomology.isoCycles₂_hom_comp_i, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, groupHomology.isoCycles₂_inv_comp_iCycles, groupCohomology.map_cochainsFunctor_shortExact, ChainComplex.mk'_X_1, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, CategoryTheory.InjectiveResolution.exact_succ, ChainComplex.mk_d, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, CochainComplex.ConnectData.comp_d₀_assoc, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, CategoryTheory.InjectiveResolution.instMonoFNatι, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, groupHomology.d₁₀ArrowIso_hom_right, Homotopy.dNext_cochainComplex, CochainComplex.mk'_d_1_0, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, ComplexShape.instHasNoLoopNatUp, groupCohomology.isoCocycles₂_hom_comp_i_apply, ChainComplex.mk'_d_1_0, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CategoryTheory.ProjectiveResolution.iso_inv_naturality, groupHomology.inhomogeneousChains.d_eq, groupHomology.eq_d₂₁_comp_inv_apply, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ, groupCohomology.cochainsFunctor_map, groupHomology.iCycles_mk, AlgebraicTopology.DoldKan.decomposition_Q, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, ComplexShape.embeddingUpIntGE_f, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, AlgebraicTopology.DoldKan.Q_f_idem_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, AlgebraicTopology.DoldKan.Γ₂N₁_inv, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, groupCohomology.cocyclesMk₀_eq, AlgebraicTopology.DoldKan.Q_f_naturality, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, AlgebraicTopology.DoldKan.Q_zero, groupHomology.lsingle_comp_chainsMap_f_assoc, ChainComplex.mkHom_f_succ_succ, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, ChainComplex.truncate_obj_X, groupCohomology.isoShortComplexH1_inv, AlgebraicTopology.DoldKan.identity_N₂_objectwise, CochainComplex.single₀_obj_zero, AlgebraicTopology.inclusionOfMooreComplexMap_f, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, CategoryTheory.Idempotents.DoldKan.hη, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', dNext_nat, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, List.toFinsupp_append, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, Finset.disjoint_range_addRightEmbedding, groupCohomology.cochainsMap_id_comp_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, CategoryTheory.ProjectiveResolution.neg_extMk, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, AlgebraicTopology.DoldKan.map_hσ', CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, AlgebraicTopology.DoldKan.N₂_map_f_f, CochainComplex.truncate_obj_d, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, groupCohomology.eq_d₁₂_comp_inv_assoc, AlgebraicTopology.DoldKan.P_f_naturality, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, CategoryTheory.SimplicialObject.Homotopy.map_homology_eq, AlgebraicTopology.DoldKan.N₁Γ₀_app, CochainComplex.isIso_homologyπ₀, groupCohomology.isoShortComplexH2_inv, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, groupCohomology.isoCocycles₂_hom_comp_i_assoc, CochainComplex.augmentTruncate_hom_f_zero, groupHomology.eq_d₁₀_comp_inv_apply, Homotopy.mkInductiveAux₂_zero, ChainComplex.alternatingConst_map_f, CategoryTheory.Idempotents.DoldKan.N_map, ChainComplex.single₀_obj_zero, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, CategoryTheory.InjectiveResolution.quasiIso, CategoryTheory.InjectiveResolution.iso_inv_naturality, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, CochainComplex.mk_d_1_0, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, groupCohomology.eq_d₀₁_comp_inv_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom, groupCohomology.isoCocycles₁_hom_comp_i_assoc, CategoryTheory.InjectiveResolution.descFOne_zero_comm, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, ChainComplex.single₀_map_f_zero, ChainComplex.alternatingConst_obj, ChainComplex.mk_d_2_1, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, AlgebraicTopology.DoldKan.Γ₀'_map_f, ComplexShape.boundaryLE_embeddingUpIntLE_iff, Rep.FiniteCyclicGroup.resolution.π_f, groupCohomology.cochainsFunctor_obj, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CochainComplex.instQuasiIsoIntπTruncGEOfIsGE, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀, CochainComplex.single₀ObjXSelf, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, CochainComplex.prev_nat_zero, AlgebraicTopology.DoldKan.Γ₂N₂_inv, groupHomology.isoCycles₂_hom_comp_i_assoc, CochainComplex.mk_X_0, groupHomology.comp_d₃₂_eq, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, groupHomology.chainsMap_f_0_comp_chainsIso₀, AlgebraicTopology.normalizedMooreComplex_obj, AlgebraicTopology.DoldKan.natTransQ_app, ChainComplex.augment_X_zero, CategoryTheory.ProjectiveResolution.complex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp_assoc, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, ComplexShape.instIsTruncGENatIntEmbeddingUpNat, CategoryTheory.instIsIsoFromLeftDerivedZero', ChainComplex.mk_X_1, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, CochainComplex.mk_X_1, groupHomology.chainsMap_f, ChainComplex.augment_d_one_zero, AlgebraicTopology.DoldKan.PInfty_add_QInfty, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, AlgebraicTopology.DoldKan.Q_f_idem, groupCohomology.cochainsMap_id, CategoryTheory.InjectiveResolution.cochainComplex_d, CochainComplex.ConnectData.restrictionGEIso_hom_f, Homotopy.mkInductiveAux₂_add_one
instAddCommMonoid 📖	CompOp	891 math math: Finset.map_nsmul_piAntidiag_univ, Finset.sum_pow_eq_sum_piAntidiag, Polynomial.coeff_prod_mem_ideal_pow_tsub, AlgebraicGeometry.AffineSpace.map_Spec_map, Finsupp.finite_of_degree_le, Behrend.sum_lt, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, KaehlerDifferential.mvPolynomialBasis_apply, MonomialOrder.sPolynomial_leadingTerm_mul', AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, MvPolynomial.isJacobsonRing, Finsupp.mapDomain_tendstoCofinite, HahnSeries.instNoZeroDivisorsFinsuppNat, MvPolynomial.totalDegree_monomial, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc, Finset.addEnergy_eq_sum_sq', CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex, MvPolynomial.radical_le_vanishingIdeal_zeroLocus, MvPolynomial.aeval_X_left, Partition.ofMultiset_parts, MvPowerSeries.weightedOrder_monomial, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, floorDiv_eq_div, AlgebraicIndependent.of_aeval, NumberField.InfinitePlace.sum_mult_eq, Finset.EquitableOn.le_add_one, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, Fin.isAddFreimanIso_Iio, roughNumbersUpTo_card_le, Algebra.Generators.H1Cotangent.δAux_mul, MvPowerSeries.coeff_mul_monomial, Algebra.Presentation.naive_toGenerators, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc, Finset.sum_filter_count_eq_countP, sum_modEq_single, MvPolynomial.isOpenMap_comap_C, MvPolynomial.universalFactorizationMap_comp_map, isLinearSet_iff_exists_matrix, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, MvPolynomial.coeff_X_mul', Algebra.PreSubmersivePresentation.ofHasCoeffs_map, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, MvPolynomial.derivation_eq_of_forall_mem_vars, Algebra.Generators.cotangentSpaceBasis_apply, finsum_one, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc, MvPolynomial.IsWeightedHomogeneous.pderiv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, Finset.sum_card_le, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, SimpleGraph.sum_degrees_eq_twice_card_edges, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, ArithmeticFunction.cardFactors_multiset_prod, Equiv.Perm.sign_of_cycleType, MvPowerSeries.coeff_pow, KaehlerDifferential.mvPolynomialBasis_repr_D_X, largeSchroder_succ, MvPolynomial.iterToSum_sumToIter, Equiv.Perm.card_of_cycleType_mul_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.pow_apply, ComplexShape.eulerCharSignsDownNat_χ, perfect_iff_sum_properDivisors, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', MvPolynomial.aeval_X_left_apply, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, MvPowerSeries.coeff_monomial_mul, CategoryTheory.InjectiveResolution.iso_hom_naturality, MvPolynomial.monomial_finsupp_sum_index, instIsOrderedAddMonoid, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, StandardEtalePresentation.toPresentation_algebra_smul, SimplexCategory.δ_comp_σ_of_gt'_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, Multiset.sum_count_eq_card, FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, MvPolynomial.image_comap_C_basicOpen, AlgebraicGeometry.Proj.mul_apply, List.sum_toFinset_count_eq_length, Finset.sum_card_fiberwise_eq_card_filter, Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe, chevalley_mvPolynomial_mvPolynomial, Sym.coe_equivNatSumOfFintype_apply_apply, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Sym.coe_equivNatSum_apply_apply, MvPolynomial.optionEquivLeft_apply, MvPolynomial.instIsScalarTower, MvPolynomial.prime_rename_iff, MvPolynomial.eval₂_prod, Finsupp.add_sub_single_one, MvPolynomial.iterToSum_C_X, MvPolynomial.map_eval₂, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, Finset.card_eq_sum_ones, Matrix.map_mul_natCast, Equiv.Perm.OnCycleFactors.kerParam_range_card, MvPolynomial.pderiv_one, MvPolynomial.mkDerivation_X, MvPolynomial.pderiv_mul, Multiset.toFinset_sum_count_eq, Behrend.sum_sq_le_of_mem_box, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Composition.sum_blocksFun, Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, Subgroup.index_eq_sum_minimalPeriod, Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst, MvPolynomial.supDegree_esymmAlgHomMonomial, Finset.even_sum_iff_even_card_odd, ArithmeticFunction.sigma_apply, cast_multiset_sum, MvPolynomial.aeval_ite_mem_eq_self, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, MvPolynomial.eval₂Hom_C_id_eq_join₁, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Algebra.Generators.algebraMap_surjective, Partition.toFinsuppAntidiag_mem_finsuppAntidiag, MvPolynomial.pow_idealOfVars, MvPolynomial.join₂_comp_map, MvPolynomial.idealOfVars_eq_restrictSupportIdeal, PolynomialLaw.toFun_eq_rTensor_φ_toFun', Behrend.map_succ, Behrend.map_le_of_mem_box, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MvPolynomial.eval_eval₂, ArithmeticFunction.sigma_one_apply_prime_pow, Rel.card_interedges_finpartition, factorization_factorial, MvPolynomial.eval₂Hom_C_eq_bind₁, Prime.emultiplicity_factorial, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, AddCommMonCat.free_map, HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top, Multiset.toFinsupp_sum_eq, MvPolynomial.mem_pow_idealOfVars_iff, MvPolynomial.X_prime, Finset.sum_nat_mod, SimplexCategory.const_subinterval_eq, AlgebraicGeometry.Proj.one_apply, Finset.map_nsmul_piAntidiag, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.pderiv_rename, IteratedWreathProduct.card, MvPolynomial.support_killCompl, Finsupp.card_toMultiset, ModEq.multisetSum_map_zero, Sym.coe_equivNatSum_symm_apply, Finset.sum_card, Polynomial.natDegree_prod', Finset.geomSum_le_geomSum_iff_toColex_le_toColex, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, Polynomial.natDegree_prod, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', Algebra.Presentation.quotientEquiv_symm, Finset.equitableOn_iff_le_le_add_one, Finset.piAntidiag_univ_fin_eq_antidiagonalTuple, MvPowerSeries.weightedOrder_monomial_of_ne_zero, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, Finset.map_sym_eq_piAntidiag, HahnSeries.toMvPowerSeries_symm_apply_coeff, MvPolynomial.sumAlgEquiv_comp_rename_inr, AlgebraicGeometry.Proj.sub_apply, geomSum_lt, sum_range_choose, Finset.count_coe_finsuppAntidiagEquiv_apply, MvPolynomial.X_mul_pderiv_monomial, Algebra.Generators.naive_val, MonomialOrder.leadingCoeff_prod_of_regular, Algebra.Generators.algebraMap_apply, corners_theorem_nat, SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges, ComplexShape.ε_down_ℕ, finSigmaFinEquiv_apply, sum_totient, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, Multiset.Nat.mem_antidiagonalTuple, Finset.sum_card_inter, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, instIsIntegralMvPolynomial, MvPolynomial.derivation_eq_zero_of_forall_mem_vars, Ideal.finrank_quotient_eq_sum, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, Sym.coe_equivNatSumOfFintype_symm_apply, SimplexCategory.δ_comp_σ_of_gt', Finset.addEnergy_eq_sum_sq, Algebra.Presentation.naive_relation, MulAction.card_eq_sum_card_group_div_card_stabilizer, SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges', Multiset.sum_nat_mod, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, Finset.sum_count_of_mem_sym, ChevalleyThm.chevalley_mvPolynomialC, Module.rankAtStalk_pi, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, Ideal.sum_ramification_inertia, Finset.mulEnergy_eq_sum_sq', Algebra.Generators.algebraMap_eq, ProjectiveSpectrum.not_irrelevant_le, instArchimedeanNat, Algebra.SubmersivePresentation.ofSubsingleton_relation, Finsupp.sub_add_single_one_cancel, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, finPiFinEquiv_apply, MvPolynomial.support_rename_of_injective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support, AlgebraicGeometry.Proj.awayι_comp_map_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, MvPolynomial.transcendental_supported_X_iff, MvPolynomial.vanishingIdeal_pointToPoint, Multiset.count_sum, AlgebraicGeometry.Proj.map_comp, MvPolynomial.algebraicIndependent_polynomial_aeval_X, isSemilinearSet_iff_ultimately_periodic, MvPolynomial.optionEquivRight_symm_apply, factorization_prod_apply, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, sum_range_multichoose, Equiv.Perm.card_of_cycleType_eq_zero_iff, properDivisors_eq_image_Iio_factorization_prod_pow, MvPolynomial.eval_prod, Polynomial.natDegree_prod_le, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, Algebra.Presentation.comp_aeval_relation_inl, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', MvPolynomial.totalDegree_finset_prod, AlgebraicGeometry.Proj.valuativeCriterion_existence, Finset.card_preimage_eq_sum_card_image_eq, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, Fin.isAddFreimanIso_Iic, Algebra.SubmersivePresentation.jacobianRelations_spec, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', MvPolynomial.pderiv_sumToIter, MvPolynomial.coeff_homogeneousComponent, Equiv.Perm.Basis.card_ofPermHom_support, MonomialOrder.coeff_prod_sum_degree, Rel.card_interedges_finpartition_right, ArithmeticFunction.sigma_apply_prime_pow, TensorProduct.toIntegralClosure_mvPolynomial_bijective, Ideal.index_pow_le, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, MvPowerSeries.coeff_inv, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.quotient_map_C_eq_zero, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, MvPolynomial.iterToSum_X, Behrend.map_apply, Setoid.IsPartition.ncard_eq_finsum, MvPolynomial.pow_idealOfVars_eq_span, Finset.sum_card_inter_le, Multiset.bell_mul_eq, Finset.le_sum_card, Finset.geomSum_ofColex_strictMono, MvPolynomial.commAlgEquiv_C, Algebra.Generators.cotangentSpaceBasis_repr_tmul, MvPolynomial.commAlgEquiv_X, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, MvPowerSeries.rename_monomial, MulAction.card_eq_sum_card_group_div_card_stabilizer', AlgebraicIndependent.lift_reprField, AlgebraicGeometry.Proj.instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, AddCommGroup.modEq_iff_natModEq, sum_conjClasses_card_eq_card, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, MvPolynomial.pderiv_X, MvPowerSeries.coeff_homogeneousComponent, ModEq.multisetSum_map, MvPolynomial.uniqueFactorizationMonoid, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, Finsupp.exists_le_degree_eq, Algebra.Generators.H1Cotangent.δAux_toAlgHom, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Fintype.card_sigma, Algebra.Presentation.naive_relation_apply, ZMod.sum_mul_div_add_sum_mul_div_eq_mul, Equiv.Perm.card_isConj_eq, fib_succ_eq_succ_sum, AlgebraicGeometry.Proj.isSeparated, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, Finset.lt_geomSum_of_mem, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, Prime.pow_dvd_factorial_iff, MvPolynomial.rename_eval₂, Finset.card_disjiUnion, MvPolynomial.coeff_sum_X_pow_of_fintype, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, MvPolynomial.finitePresentation_universalFactorizationMap, MvPolynomial.totalDegree_multiset_prod, Finsupp.finite_of_nat_weight_le, Finset.sum_card_slice, sum_properDivisors_eq_one_iff_prime, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, MvPolynomial.bind₂_id, MvPolynomial.degree_degLexDegree, MvPolynomial.sumAlgEquiv_comp_rename_inl, ArithmeticFunction.sigma_one_apply, PowerSeries.prod_monomial, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, MvPolynomial.mkDerivationₗ_monomial, Finset.card_biUnion, Finsupp.le_weight, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, ArithmeticFunction.cardFactors_eq_sum_factorization, Fin.accumulate_apply, MvPolynomial.pderiv_def, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, ceilRoot_def, MvPolynomial.mem_pow_idealOfVars_iff', Finset.toFinset_bitIndices_twoPowSum, dvd_iff_div_factorization_eq_tsub, CategoryTheory.ProjectiveResolution.iso_hom_naturality, Algebra.PreSubmersivePresentation.naive_toPresentation, Finset.sum_le_one_iff, Finset.card_filter, NumberField.totalWeight_eq_sum_mult, Equiv.Perm.card_of_cycleType, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, perfect_iff_sum_divisors_eq_two_mul, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, Finset.set_ncard_biUnion_le, cast_finsum, Finset.sum_const_nat, MvPolynomial.monomial_mem_pow_idealOfVars_iff, sum_properDivisors_dvd, fwdDiff_choose, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc, Algebra.Generators.instIsScalarTowerRing, pred_mul_geom_sum_le, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, MvPolynomial.finite_universalFactorizationMap, Finset.equivBitIndices_symm_apply, Finset.EquitableOn.le, Polynomial.degree_multiset_prod_of_monic, divisors_eq_map_attach_Iic_factorization_prod_pow, MvPolynomial.isRegular_prod_X, bell_succ', Finsupp.mapDomainEmbedding_apply, MvPolynomial.universalFactorizationMapPresentation_map, MvPolynomial.coeff_rename_mapDomain, Finsupp.multinomial_update, MvPolynomial.weightedTotalDegree_one, MvPolynomial.coeff_prod_X_pow, ArithmeticFunction.cardDistinctFactors_prod, CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, MvPolynomial.supDegree_esymm, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, MonomialOrder.sPolynomial_def, MvPolynomial.mk_eq_eval₂, Algebra.Generators.H1Cotangent.δAux_ofComp, prod_factorial_dvd_factorial_sum, MvPolynomial.killCompl_monomial_mapDomain, Polynomial.smeval_at_natCast, MvPolynomial.pointToPoint_zeroLocus_le, Finset.card_sigma, exists_integral_inj_algHom_of_quotient, factorization_ceilRoot, exists_finite_inj_algHom_of_fg, Finsupp.degree_preimage_add, MvPolynomial.coeff_monomial_mul', cast_finsum_mem, ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul, Configuration.sum_lineCount_eq_sum_pointCount, MvPowerSeries.coeff_trunc', Finset.card_eq_sum_card_image, Algebra.Generators.toAlgHom_ofComp_rename, Algebra.FinitePresentation.iff, MvPowerSeries.coeff_inv_aux, AlternatingGroup.card_of_cycleType, Equiv.Perm.sum_cycleType_le, Finsupp.DegLex.lt_iff, multiplicity_choose_aux, Polynomial.natDegree_multiset_prod, MvPolynomial.leadingCoeff_toLex_C, MvPolynomial.support_mul_X, geomSum_eq, AlgebraicGeometry.Proj.awayι_toSpecZero, MvPowerSeries.coeff_weightedHomogeneousComponent, MvPowerSeries.order_le, AlgebraicGeometry.Proj.awayToSection_comp_appLE, Finsupp.degLex_def, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, ArithmeticFunction.sum_Ioc_zeta, MvPolynomial.support_esymm', AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.isPrime_carrier, Finsupp.sum_id_lt_of_lt, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, MvPolynomial.mkₐ_eq_aeval, MvPolynomial.derivation_C, HahnSeries.toPowerSeriesAlg_apply, instIsAlgebraicMvPolynomialOfNoZeroDivisors, Multiset.count_sum', Finset.sum_range_id_mul_two, Algebra.Generators.σ_smul, MvPowerSeries.coeff_trunc, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, MvPolynomial.mkDerivation_monomial, Equiv.Perm.centralizer_le_alternating_iff, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.rename_monomial, MvPolynomial.prime_C_iff, fwdDiff_iter_choose_zero, MvPolynomial.universalFactorizationMapPresentation_relation, MvPolynomial.monic_esymm, Algebra.PreSubmersivePresentation.aevalDifferential_single, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, MvPolynomial.aeval_id_rename, isSemilinearSet_setOf_mulVec_eq, bell_succ, sum_Icc_choose, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, Equiv.Perm.card_fixedPoints, Finset.sum_antidiagonal_choose_add, sum_range_add_choose, multinomial_spec, AlgebraicGeometry.Proj.awayι_toSpecZero_assoc, MvPowerSeries.coeff_prod, Equiv.Perm.toList_formPerm_nontrivial, MvPowerSeries.exists_coeff_ne_zero_and_order, MvPolynomial.homogeneousComponent_apply, MvPolynomial.vars_prod, MvPolynomial.sumToIter_iterToSum, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, AlgebraicGeometry.Proj.zero_apply, Finset.odd_sum_iff_odd_card_odd, MvPolynomial.coeff_linearCombination_X_pow, MvPolynomial.coeff_mul_X', MvPolynomial.prod_X_pow_eq_monomial, sum_totient', Finset.card_eq_sum_card_fiberwise, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, MvPolynomial.supDegree_toLex_C, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', MvPolynomial.frobenius_zmod, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, KaehlerDifferential.mvPolynomialBasis_repr_apply, sum_divisors_eq_sum_properDivisors_add_self, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, AlgebraicGeometry.AffineSpace.map_SpecMap, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, Fintype.card_eq_sum_ones, DividedPowerAlgebra.submodule_span_prod_dp_eq_top, HahnSeries.coeff_toPowerSeries, MvPolynomial.pderiv_C_mul, Polynomial.homogenize_finsetProd, MvPolynomial.weightedHomogeneousSubmodule_one, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero, Finset.sum_pow_eq_sum_piAntidiag_of_commute, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc, Algebra.Generators.self_algebra_smul, multinomial_cons, Algebra.Generators.toKaehler_tmul_D, AddSubmonoid.isLocalizationMap_nat_int, Set.ncard_iUnion_le_of_fintype, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Multiset.count_bind, Multiset.card_sum, Polynomial.degree_prod_le, AlgebraicGeometry.Proj.opensRange_awayι, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, MvPolynomial.comap_C_surjective, cast_sum, Polynomial.degree_prod, Iio_factorization_prod_pow_injective, MvPolynomial.eval₂_eta, nat_abs_sum_le, instIsOrderedCancelAddMonoid, AlgebraicIndependent.liftAlgHom_comp_reprField, Ring.smeval_ascPochhammer_nat_cast, sum_range_choose_sq, Projectivization.card_of_finrank, Finpartition.card_bind, MonomialOrder.sPolynomial_monomial_mul, Finset.Nat.mem_antidiagonalTuple, MvPolynomial.finSuccEquiv_eq, Finset.prod_pow_eq_pow_sum, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, Module.finrank_pi_fintype, MvPolynomial.monomial_sum_index, Set.Finite.ncard_biUnion, MvPolynomial.degrees_prod_le, MvPolynomial.monic_monomial_eq, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, MvPolynomial.pderiv_monomial_single, Finset.le_sum_card_inter, MvPolynomial.degreeOf_prod_eq, multinomial_insert_one, HahnSeries.coeff_toPowerSeries_symm, MvPolynomial.IsHomogeneous.aeval, Finset.equitableOn_iff, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, Finset.sum_nsmul_assoc, smallSchroder_succ, MvPowerSeries.weightedOrder_eq_nat, instIsNoetherian, MvPowerSeries.totalDegree_trunc', padicValNat_factorial, MvPolynomial.pderiv_X_of_ne, AlgebraicGeometry.Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, MvPolynomial.prod_X_add_C_coeff, AlgebraicGeometry.Proj.add_apply, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.pderiv_monomial, multinomial_two_mul_le_mul_multinomial, Set.Finite.ncard_biUnion_le, HahnSeries.ofPowerSeriesAlg_apply_coeff, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, MvPolynomial.quotient_mk_comp_C_injective, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, AddSubmonoid.isLocalizationMap_top_nat_int, SimpleGraph.sum_degrees_support_eq_twice_card_edges, AlgebraicClosure.Monics.map_eq_prod, MonomialOrder.degree_prod_le, SimpleGraph.dart_card_eq_sum_degrees, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, MeasureTheory.upcrossingsBefore_eq_sum, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc, card_sigma, HomogeneousLocalization.Away.isLocalization_mul, MvPolynomial.aeval_eq_bind₁, Polynomial.degree_multiset_prod_le, Polynomial.degree_prod_of_monic, Finset.mulEnergy_eq_sum_sq, Finsupp.degree_preimage_nsmul, cast_finsupp_sum, PowerSeries.coeff_prod, MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, Multiset.bell_eq, List.Nat.mem_antidiagonalTuple, MvPolynomial.IsWeightedHomogeneous.prod, Algebra.Generators.repr_CotangentSpaceMap, DividedPowerAlgebra.dp_sum_smul, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, MvPolynomial.pderiv_pow, MvPowerSeries.algebraMap_apply', HahnSeries.coeff_toMvPowerSeries_symm, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, StandardEtalePresentation.toPresentation_σ', CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, MvPolynomial.weightedTotalDegree_piSingle, MvPolynomial.isIntegral_iff_isIntegral_coeff, witt_structure_prop, MvPowerSeries.weightedOrder_le, factorization_floorRoot, MvPolynomial.eval₂Hom_eq_bind₂, floorRoot_def, MvPolynomial.prod_C_add_X_eq_sum_esymm, Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, MvPolynomial.eval₂_map_comp_C, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, ComplexShape.eulerCharSignsUpNat_χ, LinearMap.snd_prodOfFinsuppNat, Finset.twoPowSum_toFinset_bitIndices, DividedPowerAlgebra.dp_sum, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, MvPolynomial.sumAlgEquiv_apply, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, Algebra.Generators.ker_comp_eq_sup, AlgebraicGeometry.stalkToFiberRingHom_germ, MvPolynomial.sumToIter_Xr, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', MvPolynomial.algebraicIndependent_X, AlgebraicGeometry.Proj.awayMap_awayToSection, MvPolynomial.esymmAlgHom_apply, MvPolynomial.monomial_eq, MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, MvPolynomial.rename_prod_mk_eval₂, factorization_div, AlgebraicIndependent.aevalEquivField_apply_coe, IsTranscendenceBasis.mvPolynomial, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, MvPolynomial.pderiv_map, MvPowerSeries.coeff_invOfUnit, Algebra.Generators.naive_σ, MvPolynomial.esymm_eq_sum_monomial, Finsupp.toMultiset_sum, Set.ncard_iUnion_of_finite, ArithmeticFunction.mul_zeta_apply, sum_divisors, Finsupp.range_single_one, Module.finrank_directSum, fib_succ_eq_sum_choose, Finset.card_finsuppAntidiag_nat_eq_multichoose, MvPolynomial.totalDegree_monomial_le, MvPowerSeries.totalDegree_truncFinset, AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup, multinomial_insert, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, MvPolynomial.pderiv_inr_universalFactorizationMap_X, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, MvPolynomial.sumAlgEquiv_symm_apply, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, geom_sum_le, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, MvPolynomial.instIsPushout_1, Finset.card_biUnion_le, MvPolynomial.C_mem_pow_idealOfVars_iff, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, Algebra.Generators.toExtension_algebra₁, KaehlerDifferential.mvPolynomialBasis_repr_D, MonomialOrder.sPolynomial_monomial_mul', HahnSeries.coeff_toMvPowerSeries, MvPolynomial.pderiv_eq_zero_of_notMem_vars, Finset.Nat.antidiagonal_filter_le_fst_of_le, MvPolynomial.support_divMonomial, MvPolynomial.aeval_C_comp_left, Prime.multiplicity_factorial_pow, MvPowerSeries.order_monomial, AlgebraicGeometry.Proj.valuativeCriterion_existence_aux, AlgebraicGeometry.Proj.stalkIso'_germ, sub_one_mul_sum_div_pow_eq_sub_sum_digits, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, MvPolynomial.mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, sum_modEq_ite, Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, Finset.Nat.antidiagonal_filter_snd_le_of_le, MvPolynomial.isLocalization_C_mk', AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant, Equiv.Perm.card_le_of_centralizer_le_alternating, MvPolynomial.eval₂Hom_id_X_eq_join₂, Algebra.Generators.Hom.comp_val, MvPolynomial.instIsPushout, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, catalan_succ, MvPolynomial.esymm_eq_multiset_esymm, AlgebraicGeometry.AffineSpace.over_over, Rel.card_interedges_finpartition_left, Finsupp.weight_sub_single_add, IsTranscendenceBasis.mvPolynomial', AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun_asIdeal, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, MvPolynomial.support_esymm'', MvPolynomial.isLocalization, StandardEtalePresentation.toPresentation_val, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, finSigmaFinEquiv_one, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly, Finset.sum_range_id, abundant_iff_sum_divisors, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, MvPolynomial.aeval_id_eq_join₁, Finset.card_shatterer_le_sum_vcDim, SSet.δ_comp_σ_of_gt'_apply, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, MvPolynomial.le_totalDegree, Algebra.mvPolynomial, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors, MonomialOrder.degree_prod, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, Submodule.finrank_quotient_eq_sum, Equiv.Perm.exists_with_cycleType_iff, MvPolynomial.prod_X_pow, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, MvPolynomial.IsHomogeneous.sum_X_mul_pderiv, MvPolynomial.derivation_C_mul, MvPolynomial.aeval_sumElim_pderiv_inl, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', Multiset.card_join, MvPolynomial.iterToSum_C_C, HahnSeries.ofPowerSeries_apply, sum_sum_digits_eq, MvPolynomial.eval₂_C_mk_eq_zero, MvPolynomial.universalFactorizationMap_freeMonic, Algebra.Generators.Hom.toAlgHom_monomial, MvPolynomial.universalFactorizationMapPresentation_val, catalan_succ', sum_range_mul_choose, HahnSeries.toMvPowerSeries_apply, MvPolynomial.coe_expand, ZMod.eisenstein_lemma, MvPolynomial.aeval_sumElim, MvPolynomial.universalFactorizationMapPresentation_σ', KaehlerDifferential.mvPolynomialBasis_repr_symm_single, Finpartition.sum_card_parts, Partition.parts_sum, properDivisors_eq_map_attach_Iio_factorization_prod_pow, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Finsupp.DegLex.le_iff, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, MvPolynomial.coeff_linearCombination_X_pow_of_fintype, MvPolynomial.monomial_sum_one, ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div, Algebra.Presentation.quotientEquiv_mk, AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer, finFunctionFinEquiv_apply_val, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, Polynomial.natDegree_multiset_prod', Polynomial.natDegree_prod_of_monic, MvPolynomial.weightedTotalDegree_rename_of_injective, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, MvPolynomial.IsHomogeneous.prod, MvPowerSeries.order_eq_nat, ceilDiv_eq_add_pred_div, MvPolynomial.IsSymmetric.antitone_supDegree, sum_range_choose_halfway, MvPowerSeries.coeff_rename, Int.natAbs_sum_le, CategoryTheory.ProjectiveResolution.iso_inv_naturality, MvPolynomial.isJacobsonRing_MvPolynomial_fin, MvPolynomial.degreeOf_prod_le, AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer', MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply, Polynomial.natDegree_multiset_prod_le, AlgebraicGeometry.Proj.instIsOpenImmersionAwayι, MonomialOrder.sPolynomial_mem_sup_ideal, MvPolynomial.join₂_map, MvPolynomial.eval₂Hom_C_left, ModEq.sum_zero, Multiset.card_finsuppSum, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, StandardEtalePresentation.toPresentation_relation, MvPolynomial.leadingCoeff_toLex, Finset.Nat.antidiagonal_filter_fst_le_of_le, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Equiv.Perm.sum_cycleType, Algebra.Generators.self_algebra_algebraMap, MvPolynomial.esymm_eq_sum_subtype, MvPolynomial.coeff_mul_monomial', MonomialOrder.Monic.prod, MvPolynomial.ringKrullDim_of_isNoetherianRing, MvPolynomial.pderiv_X_self, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, MvPolynomial.pderiv_C, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Polynomial.degree_multiset_prod, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, MvRatFunc.rank_eq_max_lift, MvPolynomial.aeval_prod, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, sum_card_addOrderOf_eq_card_nsmul_eq_zero, exists_signed_sum, Finsupp.sub_single_one_add, Group.nat_card_center_add_sum_card_noncenter_eq_card, Finset.Nat.antidiagonal_filter_le_snd_of_le, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, DividedPowers.prod_dpow, Finsupp.DegLex.monotone_degree, Finset.finsuppAntidiagEquiv_symm_apply_apply, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, ArithmeticFunction.zeta_mul_apply, AlternatingGroup.map_subtype_of_cycleType, MvPolynomial.sumToIter_C, PowerSeries.coeff_pow, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, HahnSeries.toPowerSeries_apply, MvPowerSeries.monomial_smul_const, MvPolynomial.derivation_eqOn_supported, Polynomial.natDegree_multiset_prod_of_monic, MvPolynomial.IsHomogeneous.eval₂, Coprime.sum_divisors_mul, MonomialOrder.degree_prod_of_regular, MvPolynomial.trdeg_of_isDomain, Group.card_center_add_sum_card_noncenter_eq_card, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, MvPolynomial.support_esymm, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, finFunctionFinEquiv_apply, MvPolynomial.transcendental_supported_X, AlgebraicGeometry.Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Multiset.card_bind, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, HomogeneousLocalization.Away.finiteType, AlgebraicGeometry.Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Finsupp.nsmul_single_one_image, Finsupp.DegLex.lt_def, HahnSeries.toPowerSeries_symm_apply_coeff, sum_card_orderOf_eq_card_pow_eq_one, Algebra.Generators.comp_σ, sum_div, Finsupp.sum_eq_one_iff, ZMod.eisenstein_lemma_aux, AlgebraicGeometry.Proj.stalkIso'_symm_mk, MvPowerSeries.order_monomial_of_ne_zero, Algebra.Presentation.instFinitePresentationQuotientOfFinite, ArithmeticFunction.sigma_eq_sum_div, MvPolynomial.eval₂_assoc, Finsupp.toMultiset_sum_single, factorization_prod, DividedPowerAlgebra.prod_dp, exists_integral_inj_algHom_of_fg, MvPolynomial.coeff_rename_ne_zero, FiniteField.algebraMap_norm_eq_pow_sum, ENat.toNat_sum, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso, CategoryTheory.InjectiveResolution.iso_inv_naturality, Finsupp.toMultiset_map, FirstOrder.Language.presburger.term_realize_eq_add_dotProduct, MvPolynomial.eval_assoc, add_choose_eq, MvPolynomial.support_X_mul, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, Algebra.Generators.ker_naive, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, instFreeMvPolynomialKaehlerDifferential, AlternatingGroup.card_of_cycleType_mul_eq, Finset.geomSum_injective, rank_mvPolynomial_mvPolynomial, FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinear, ModEq.multisetSum_zero, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, MvPolynomial.algebraMap_def, Group.sum_card_conj_classes_eq_card, AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective, fwdDiff_iter_choose, Equiv.Perm.card_isConj_mul_eq, geom_sum_Ico_le, MvPolynomial.rename_eq, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, Equiv.Perm.nat_card_centralizer, MvPolynomial.derivation_ext_iff, CategoryTheory.InjectiveResolution.rightDerived_app_eq, ringKrullDim_mvPolynomial_of_isEmpty, MvPolynomial.IsHomogeneous.pderiv, FirstOrder.Language.presburger.definable_iff_isSemilinearSet, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt', AlgebraicGeometry.Proj.awayι_comp_map, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bind₁_monomial, MvPolynomial.mem_image_comap_C_basicOpen, Algebra.Presentation.mem_ker_naive, SimpleGraph.isBipartiteWith_sum_degrees_eq, MvPolynomial.coeff_killCompl, Iic_factorization_prod_pow_injective, Behrend.sum_eq, instIsPushoutFractionRingMvPolynomial_1, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.degree_prod_of_mem_nonZeroDivisors, Algebra.Generators.toExtension_commRing, MvPowerSeries.prod_monomial, ModEq.sum, MvPolynomial.decomposition.decompose'_eq, MvPolynomial.universalFactorizationMapPresentation_jacobian, MonomialOrder.sPolynomial_leadingTerm_mul, MvPolynomial.commAlgEquiv_C_X, Finset.card_finsuppAntidiag_nat_eq_choose, List.sum_fixedLengthDigits_sum, Finset.nsmul_piAntidiag_univ, Multiset.card_sigma, Set.ncard_iUnion_le_of_finite, MvPolynomial.transcendental_supported_polynomial_aeval_X, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom, instIsPushoutFractionRingMvPolynomial, MvPolynomial.sumToIter_Xl, Finsupp.image_pow_eq_finsuppProd_image, SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges, MvPolynomial.pderiv_inl_universalFactorizationMap_X, divisors_eq_image_Iic_factorization_prod_pow, Finset.nsmul_piAntidiag, MvPolynomial.instFaithfulSMul, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val
instAddCommSemigroup 📖	CompOp	48 math math: CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, Polynomial.sylvester_comm, ComplexShape.eulerCharSignsDownNat_χ, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.iso_hom_naturality, SimplexCategory.δ_comp_σ_of_gt'_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, SimplexCategory.const_subinterval_eq, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, ComplexShape.ε_down_ℕ, SimplexCategory.δ_comp_σ_of_gt', FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_snd_coe, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, precomp_extClass_surjective_of_projective_X₂, CategoryTheory.ProjectiveResolution.iso_hom_naturality, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, MvPolynomial.support_mul_X, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, Sym.append_comm, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, ComplexShape.eulerCharSignsUpNat_χ, LinearMap.snd_prodOfFinsuppNat, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, Finset.Nat.antidiagonal_filter_le_fst_of_le, Finset.Nat.antidiagonal_filter_snd_le_of_le, SSet.δ_comp_σ_of_gt'_apply, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, Composition.reverse_append, CategoryTheory.ProjectiveResolution.iso_inv_naturality, Finset.Nat.antidiagonal_filter_fst_le_of_le, Finset.Nat.antidiagonal_filter_le_snd_of_le, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, CategoryTheory.InjectiveResolution.iso_inv_naturality, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'
instAddMonoid 📖	CompOp	1897 math math: Finset.map_nsmul_piAntidiag_univ, MvPolynomial.is_id, IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, Finsupp.image_prodMap_embDomain_antidiagonal, MvPolynomial.pUnitAlgEquiv_symm_monomial, MvPolynomial.funext_iff, MvPolynomial.eval_indicator_apply_eq_one, Height.logHeight_eval_ge, MvPolynomial.join₁_rename, MvPolynomial.vanishingIdeal_anti_mono, MvPolynomial.eval₂_mul_eq_zero_of_left, MvPolynomial.aeval_sum, Finsupp.sum_toMultiset, MvPolynomial.dvd_monomial_one_iff_exists, WittVector.bind₁_frobeniusPoly_wittPolynomial, MonomialOrder.le_degree_of_mem_support, TensorAlgebra.ofDirectSum_of_tprod, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', KaehlerDifferential.mvPolynomialBasis_apply, MonomialOrder.sPolynomial_leadingTerm_mul', MvPolynomial.coe_C, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, MvPolynomial.support_mul, MvPolynomial.algHom_ext_iff, MonomialOrder.span_leadingTerm_sdiff_singleton_zero, MvPolynomial.map_bind₁, DFinsupp.toMultiset_sup, rothNumberNat_spec, Algebra.Generators.aeval_val_surjective, MvPolynomial.mul_X_divMonomial, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, ProjectiveSpectrum.mem_basicOpen, wittPolynomial_zmod_self, LieDerivation.iterate_apply_lie, MvPolynomial.aeval_X_left, MvPolynomial.map_mapRange_eq_iff, Finset.Nat.sum_antidiagonal_eq_sum_range_succ, MvPolynomial.map_comp_C, MvPolynomial.coeffs_add, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, MvPolynomial.pUnitAlgEquiv_apply, ExteriorAlgebra.GradedAlgebra.liftι_eq, Finset.Nat.antidiagonal_eq_image', MvPolynomial.eval₂Hom_X, floorDiv_eq_div, MvPolynomial.toMvPowerSeries_uniformContinuous, MvPolynomial.exists_finset_rename, MonomialOrder.monic_X_sub_C, MvPolynomial.hom_C, Polynomial.homogenize_map, MvPolynomial.support_finSuccEquiv, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, MvPolynomial.degrees_monomial, MvPolynomial.zero_divMonomial, Ideal.mem_span_iff_exists_isHomogeneous, MvPolynomial.coeff_divMonomial, WittVector.aeval_verschiebung_poly', FreeAddMonoid.count_apply, MonomialOrder.degree_add_of_ne, MvPolynomial.rTensorAlgEquiv_apply, Algebra.Generators.H1Cotangent.δAux_mul, Algebra.Presentation.naive_toGenerators, Multiset.toFinsupp_add, MvPolynomial.mem_image_support_coeff_finSuccEquiv, MvPolynomial.mapEquiv_symm, Finsupp.toMultiset_strictMono, MvPolynomial.comapEquiv_symm_coe, MvPolynomial.homogeneousComponent_eq_zero', WeierstrassCurve.Projective.eval_polynomial, Matrix.charpoly.univ_map_map, MvPolynomial.eval₂_expand, ChevalleyThm.MvPolynomialC.degBound_casesOn_succ, Finset.Nat.sum_antidiagonal_subst, MvPolynomial.universalFactorizationMap_comp_map, MvPolynomial.aeval_algebraMap_eq_zero_iff, MvPowerSeries.support_expand, MvPolynomial.coeff_X_mul', Algebra.PreSubmersivePresentation.ofHasCoeffs_map, MvPolynomial.expand_X, Multiset.equivDFinsupp_symm_apply, algebraicIndependent_iff_ker_eq_bot, factorization_pow, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, MvPolynomial.IsSymmetric.map, Algebra.Generators.cotangentSpaceBasis_apply, Polynomial.toFinsupp_zsmul, Finset.Nat.prod_antidiagonal_succ, Multiset.toDFinsupp_support, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc, MvPolynomial.instIsReduced, MvPolynomial.X_pow_eq_monomial, MvPolynomial.isEmptyRingEquiv_apply, WittVector.ghostComponent_apply, MvPolynomial.ker_map, MvPolynomial.map_leftInverse, aeval_wittPolynomial, AddSubmonoid.mem_closure_finset, MvPolynomial.aeval_range, Mathlib.Tactic.Ring.smul_nat, KaehlerDifferential.mvPolynomialBasis_repr_D_X, MvPolynomial.optionEquivLeft_C, MvPolynomial.rename_rename, ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, MvPolynomial.iterToSum_sumToIter, constantCoeff_wittStructureRat, AlgebraicGeometry.Proj.isLocallyFraction_comapStructureSheafFun, Algebra.Generators.toAlgHom_ofComp_localizationAway, Finset.sum_antidiagonal_choose_succ_mul, Finset.Nat.prod_antidiagonal_swap, MvPolynomial.leibniz_iff_X, ProjectiveSpectrum.gc_homogeneousIdeal, AlgebraicGeometry.Proj.pow_apply, ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal, Polynomial.degree_pow_le, MvPolynomial.divMonomial_add_modMonomial, CategoryTheory.Abelian.Ext.precomp_mk₀_injective_of_epi, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', MvPowerSeries.trunc'_expand_trunc', MvPolynomial.optionEquivLeft_X_some, MonomialOrder.leadingCoeff_eq_zero_iff, MvPolynomial.eval₂Hom_monomial, IsCyclotomicExtension.discr_odd_prime, Polynomial.toFinsupp_pow, MvPolynomial.homogeneousComponent_of_mem, MvPolynomial.aeval_X_left_apply, Polynomial.toPowerSeries_toMvPowerSeries, Tree.treesOfNumNodesEq_succ, MvPolynomial.le_vanishingIdeal_zeroLocus, MvPolynomial.pUnitAlgEquiv_symm_apply, FreeAddMonoid.count_of, MvPolynomial.expand_eq_zero, ProjectiveSpectrum.vanishingIdeal_iUnion, WeierstrassCurve.Jacobian.baseChange_polynomialZ, TensorAlgebra.toDirectSum_tensorPower_tprod, Algebra.Presentation.localizationAway_relation, MvPolynomial.monomial_finsupp_sum_index, MvPolynomial.weightedHomogeneousSubmodule_mul, Ideal.span_pow_eq_map_homogeneousSubmodule, MvPolynomial.coeffs_mul_X, Polynomial.degree_pow, MvPolynomial.mul_def, MvPolynomial.natDegree_finSuccEquiv, Finsupp.prod_toMultiset, StandardEtalePresentation.toPresentation_algebra_smul, cyclotomicCharacter.toZModPow, frobeniusNumber_iff, MvPolynomial.totalDegree_X_pow, Ideal.span_eq_map_homogeneousSubmodule, Finset.Nat.antidiagonal_succ_succ', Finsupp.toMultiset_zero, MvPolynomial.bind₂_comp_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, MvPolynomial.eval₂_zero'_apply, AlgebraicGeometry.Proj.mul_apply, MvPolynomial.degreeOf_C, WeierstrassCurve.Projective.polynomial_relation, Matrix.toMvPolynomial_add, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply, CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, MvPolynomial.algHom_ext'_iff, IntermediateField.mem_adjoin_iff, AlgebraicIndependent.repr_ker, MonomialOrder.leadingCoeff_mul_of_isRegular_right, chevalley_mvPolynomial_mvPolynomial, MvPolynomial.mem_range_map_iff_coeffs_subset, MvPolynomial.aeval_X, MvPolynomial.comapEquiv_coe, MvPolynomial.vars_sub_of_disjoint, MvPolynomial.exists_dvd_map_of_isAlgebraic, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, MvPolynomial.eval₂_pow, MvPolynomial.irreducible_mul_X_add, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, MonomialOrder.leadingCoeff_mul, MonomialOrder.degree_sub_le, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, AnalyticOnNhd.eval_linearMap', MvPolynomial.optionEquivLeft_apply, MvPolynomial.instIsScalarTower, MvPolynomial.bind₂_C_left, MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le, Multiset.Icc_eq, MvPolynomial.map_comp_rename, MvPolynomial.ACounit_X, WittVector.mul_polyOfInterest_aux2, MvPolynomial.prime_rename_iff, multiplesAddHom_apply, Polynomial.eval_eq_div_eval_toTupleMvPolynomial, bind₁_xInTermsOfW_wittPolynomial, WeierstrassCurve.Jacobian.eval_polynomialY, FreeMonoid.countP_of, IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two, MvPolynomial.constantCoeff_rename, exists_mem_closure_of_ge, uliftMultiplesHom_symm_apply, CategoryTheory.Abelian.Ext.mk₀_id_comp, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, MvPolynomial.map_bind₂, List.sum_map_count_dedup_eq_length, Finsupp.add_sub_single_one, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, MvPolynomial.iterToSum_C_X, AlgebraicClosure.maxIdeal.isMaximal, MvPolynomial.map_eval₂, MvPolynomial.eval_map, CommRingCat.free_map_coe, Algebra.FinitePresentation.mvPolynomial_of_finitePresentation, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', MvPolynomial.killCompl_comp_rename, MvPolynomial.map_eval₂Hom, MvPolynomial.supportedEquivMvPolynomial_symm_X, Finset.Nat.antidiagonal_eq_image, MvPolynomial.pderiv_one, MvPolynomial.pderiv_mul, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, char_dvd_card_solutions_of_add_lt, MvPolynomial.comp_eval₂Hom, MvPolynomial.ACounit_surjective, MvPolynomial.supported_eq_adjoin_X, MonomialOrder.degree_lt_iff, MvPolynomial.eval₂_zero, MvPolynomial.degreeOf_mul_le, Finset.Nat.antidiagonalEquivFin_symm_apply_coe, Ring.add_choose_eq, MvPolynomial.aeval_eq_eval, MvPolynomial.supDegree_esymmAlgHomMonomial, MvPolynomial.schwartz_zippel_totalDegree, MvPolynomial.aeval_ite_mem_eq_self, MvPolynomial.support_sdiff_support_subset_support_add, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, MvPolynomial.IsWeightedHomogeneous.mul, MvPolynomial.eval₂Hom_C_id_eq_join₁, Finsupp.toMultiset_toFinsupp, MvPolynomial.eval_mem, PolynomialLaw.exists_lift', ax_grothendieck_of_definable, Behrend.map_mod, MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt, MvPolynomial.pow_idealOfVars, MvPolynomial.join₂_comp_map, PolynomialLaw.toFun_eq_rTensor_φ_toFun', MvPolynomial.comap_id, Height.logHeight_eval_ge', MvPolynomial.eval_rename_prod_mk, Behrend.map_succ, MvPolynomial.optionEquivRight_C, Behrend.map_le_of_mem_box, MvPolynomial.monomial_zero, MvPolynomial.map_mvPolynomial_eq_eval₂, ProjectiveSpectrum.sup_vanishingIdeal_le, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MonomialOrder.degree_reduce_lt, MvPolynomial.eval_eval₂, MvPolynomial.aevalTower_comp_C, MvPolynomial.totalDegree_eq, MvPolynomial.rename_msymm, MvPolynomial.comap_comp_apply, MvPolynomial.eval₂_id, MvPolynomial.eval₂Hom_C_eq_bind₁, ProjectiveSpectrum.mem_vanishingIdeal, MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero, MvPolynomial.X_mul_cancel_right_iff, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, MvPolynomial.degreeOf_coeff_finSuccEquiv, HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top, Multiset.toFinsupp_sum_eq, MvPolynomial.mem_pow_idealOfVars_iff, Multiset.toDFinsupp_apply, List.length_le_sum_of_one_le, MvPolynomial.rename_id_apply, MvPolynomial.constantCoeff_C, AlgebraicGeometry.Proj.one_apply, MvPowerSeries.trunc_C, MvPolynomial.map_map, MvPolynomial.support_eq_empty, Finset.map_nsmul_piAntidiag, MvPolynomial.eval₂Hom_comp_bind₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, MvPolynomial.degrees_def, Finset.Nat.antidiagonal_eq_map, MvPolynomial.nonempty_support_finSuccEquiv, Finset.Nat.antidiagonal_succ, Polynomial.eval₂_ofFinsupp, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.mvPolynomialEquivMvPolynomial_apply, MvPolynomial.pderiv_rename, Algebra.Presentation.comp_relation_inr, MonomialOrder.toSyn_strictMono, LinearMap.nilRankAux_basis_indep, MonomialOrder.leadingTerm_zero, MvPolynomial.eval₂_mul_monomial, MvPolynomial.weightedHomogeneousComponent_zero, MvPolynomial.support_killCompl, AlgebraicIndependent.aeval_comp_repr, MonomialOrder.div_single, MvPolynomial.esymmAlgHomMonomial_single, MvPolynomial.homogeneousComponent_C_mul, Polynomial.ofFinsupp_natCast, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, MvPolynomial.IsHomogeneous.map, PowerSeries.support_expand_subset, MvPolynomial.map_expand, MonomialOrder.image_leadingTerm_sdiff_singleton_zero, Finsupp.card_toMultiset, DividedPowers.OfInvertibleFactorial.dpow_add, MvPolynomial.map_aeval, Sym.coe_equivNatSum_symm_apply, MvPolynomial.map_frobenius_expand, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow, MvPolynomial.renameEquiv_trans, Height.logHeight_eval_le', FirstOrder.Ring.lift_genericPolyMap, multiplesAddHom_symm_apply, SkewPolynomial.φ_iterate_apply, MvPolynomial.expand_monomial, List.tail_sum, MvPolynomial.expand_char, MvPolynomial.monomial_mul_mem_coeffsIn, MvPolynomial.eval₂Hom_congr, IsCyclotomicExtension.Rat.discr_prime_pow', WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, MvPolynomial.map_rename, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, powersHom_symm_apply, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', MvPolynomial.killCompl_C, Algebra.Presentation.quotientEquiv_symm, MvPolynomial.eval₂_const_pUnitAlgEquiv_symm, MvPolynomial.eval_comp_toMvPolynomial, TensorPower.algebraMap₀_mul, Algebra.Generators.H1Cotangent.δAux_C, Algebra.Generators.map_toComp_ker, MvPolynomial.support_finSuccEquiv_nonempty, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, PowerSeries.support_expand, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, MvPolynomial.bind₁_X_left, PowerSeries.coeff_inv_aux, MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero, MvPolynomial.sumAlgEquiv_comp_rename_inr, TensorAlgebra.toDirectSum_ofDirectSum, factorization_mul, MvPolynomial.aevalTower_toAlgHom, AlgebraicGeometry.Proj.sub_apply, Algebra.Generators.ofComp_val, Polynomial.ofFinsupp_sub, Algebra.Presentation.map_relationOfHasCoeffs, LinearMap.polyCharpoly_coeff_isHomogeneous, MvPolynomial.eval₂_map, MvPolynomial.X_mul_pderiv_monomial, MvPowerSeries.lexOrder_def_of_ne_zero, MonomialOrder.degree_add_le, MvPolynomial.degree_optionEquivLeft, MvPolynomial.mapAlgHom_id, Algebra.Generators.naive_val, MvPolynomial.totalDegree_list_prod, Multiset.equivDFinsupp_apply, MvPolynomial.coeff_expand_smul, Algebra.Generators.algebraMap_apply, Finset.Nat.prod_antidiagonal_eq_prod_range_succ, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂', MvPolynomial.map_esymm, ComplexShape.ε_down_ℕ, MvPolynomial.weightedHomogeneousComponent_eq_zero', MvPolynomial.IsHomogeneous.add, MvPolynomial.coe_eq_zero_iff, DFinsupp.toMultiset_single, MvPolynomial.expand_C, factorization_mul, nsmul_eq_mul, MonomialOrder.eq_C_of_degree_eq_zero, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two, addSubmonoidClosure_one, instIsIntegralMvPolynomial, MvPolynomial.coeffs_C, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, MvPolynomial.optionEquivRight_X_none, MvPolynomial.rename_psum, Algebra.Generators.map_ofComp_ker, Finsupp.toMultiset_apply, MvPowerSeries.lexOrder_mul, Finset.sum_antidiagonal_choose_succ_nsmul, WeierstrassCurve.Jacobian.polynomialY_eq, MvPolynomial.expand_zero, addUnits_eq_zero, MvPolynomial.support_add, MonomialOrder.sPolynomial_self, uliftPowersHom_symm_apply, MvPolynomial.degreesLE_nsmul, WeierstrassCurve.Jacobian.eval_polynomialX, MvPolynomial.totalDegree_rename_le, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, MvPolynomial.C_apply, MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, MvPolynomial.coe_mapEquivMonic_comp', Algebra.Presentation.naive_relation, WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Projective.baseChange_polynomial, AlgebraicGeometry.Proj.mem_basicOpen, isAddUnit_iff, Matrix.toMvPolynomial_map, Polynomial.toMvPolynomial_eq_rename_comp, DividedPowerAlgebra.dp_mul, MonomialOrder.le_degree, Polynomial.ofFinsupp_pow, Polynomial.aeval_homogenize_X_one, MvPolynomial.adjoin_range_X, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, MvPolynomial.mul_X_mem_coeffsIn, MvPolynomial.coeff_C, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, MvPolynomial.bind₂_map, MvPolynomial.totalDegree_mul_of_isDomain, Finsupp.antidiagonal_single, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, MvPolynomial.X_dvd_X, MvPolynomial.transcendental_polynomial_aeval_X_iff, MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective, Algebra.Generators.algebraMap_eq, PowerSeries.coeff_invOfUnit, constantCoeff_wittStructureInt, Finset.Nat.antidiagonalTuple_two, Algebra.SubmersivePresentation.ofSubsingleton_relation, Finsupp.sub_add_single_one_cancel, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, MvPolynomial.X_mul_mem_coeffsIn, MvPolynomial.support_rename_of_injective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, MvPolynomial.comap_comp, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, MvPolynomial.eval_ofNat, MonomialOrder.degree_mul_leadingTerm, xInTermsOfW_eq, LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree, MvPolynomial.eval_eq_eval_mv_eval', MvPolynomial.degrees_map_of_injective, MvPolynomial.ACounit_C, LinearMap.polyCharpoly_baseChange, MvPolynomial.eq_zero_of_eval_eq_zero, MvPolynomial.transcendental_supported_X_iff, Polynomial.homogenize_add, ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal, MvPolynomial.optionEquivLeft_X_none, MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul, MvPolynomial.algebraicIndependent_polynomial_aeval_X, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁', Submonoid.closure_singleton_eq, MonoidHom.apply_mnat, MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring, MvPolynomial.degreeOf_rename_of_injective, MvPolynomial.degreesLE_add, MvPolynomial.exists_rename_eq_of_vars_subset_range, MonomialOrder.span_leadingTerm_eq_span_monomial, MvPolynomial.optionEquivRight_symm_apply, MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet, MvPolynomial.eval₂Hom_zero_apply, Multiset.toFinsupp_union, MonomialOrder.span_leadingTerm_eq_span_monomial₀, MvPolynomial.degrees_C, WeierstrassCurve.Jacobian.polynomial_relation, LinearMap.polyCharpolyAux_map_eval, AddSubmonoid.mem_closure_iff_exists_finset_subset, MvPolynomial.eval_prod, LinearMap.polyCharpoly_coeff_eq_zero_of_basis, Finset.Nat.card_antidiagonal, MvPolynomial.C_mul_X_eq_monomial, Algebra.Generators.Hom.aeval_val, CategoryTheory.ProjectiveResolution.extMk_comp_mk₀, Polynomial.MonicDegreeEq.freeMonic_coe, Polynomial.ofFinsupp_algebraMap, DividedPowerAlgebra.natFactorial_mul_dp_eq, MvPolynomial.degreeOf_mul_eq, TensorAlgebra.equivDirectSum_apply, Algebra.Presentation.comp_aeval_relation_inl, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', MvPolynomial.C_0, WittVector.mulN_coeff, MvPolynomial.bind₂_monomial, MvPolynomial.isUnit_iff_totalDegree_of_isReduced, MvPolynomial.monomialOneHom_apply, Fin.accumulate_invAccumulate, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, Algebra.SubmersivePresentation.jacobianRelations_spec, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', MvPolynomial.pderiv_sumToIter, MvPolynomial.support_expand_subset, MvPolynomial.totalDegree_C, LinearMap.toMvPolynomial_add, WeierstrassCurve.Projective.polynomialZ_eq, MonomialOrder.lex_lt_iff_of_unique, Matrix.charpoly.univ_monic, MvPolynomial.totalDegree_pow, MvPolynomial.coeff_rename_embDomain, MvPolynomial.isUnit_iff, MvPolynomial.X_dvd_monomial, MvPolynomial.coe_zero, MonomialOrder.degLex_le_iff, MvPolynomial.finSuccEquiv_coeff_coeff, MvPolynomial.rename_comp_expand, Behrend.map_injOn, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem', Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, ProjectiveSpectrum.isPrime, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', MvPowerSeries.coeff_inv, MvPolynomial.coeff_C_mul, MvPolynomial.rename_esymm, MvPolynomial.IsHomogeneous.sub, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.quotient_map_C_eq_zero, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, MvPolynomial.iterToSum_X, MvPolynomial.coeff_X_pow, MvPolynomial.C_mul_monomial, Finset.Nat.antidiagonal_zero, Behrend.map_apply, MvPolynomial.pow_idealOfVars_eq_span, AnalyticOnNhd.eval_linearMap, MvPolynomial.IsHomogeneous.pow, DividedPowers.dpow_add, SkewPolynomial.φ_def, Algebra.Generators.toAlgHom_ofComp_surjective, MvPolynomial.bind₁_comp_bind₁, MvPolynomial.commAlgEquiv_C, MvPolynomial.coeff_zero_C, Algebra.Generators.Hom.algebraMap_toAlgHom', CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, Algebra.FinitePresentation.ker_fg_of_mvPolynomial, Algebra.Generators.cotangentSpaceBasis_repr_tmul, MonomialOrder.monic_X_add_C, bernoulli_spec', MvPolynomial.aevalTower_X, MvPolynomial.vars_sub_subset, AddSubmonoid.closure_singleton_eq, MvPolynomial.bind₂_monomial_one, MvPolynomial.irreducible_of_forall_totalDegree_le, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc, MvPolynomial.commAlgEquiv_X, threeAPFree_iff_eq_right, MvPolynomial.mapEquiv_apply, MvPolynomial.eval₂Hom_congr', Matrix.charpoly.univ_coeff_eval₂Hom, Multiset.toFinsupp_inter, MvPolynomial.optionEquivRight_X_some, Polynomial.toFinsupp_nsmul, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, MonomialOrder.degree_le_iff, ZMod.card_units, MvPolynomial.aeval_expand, AlgebraicIndependent.lift_reprField, MvPolynomial.instCharZero, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, MvPolynomial.aeval_algebraMap_apply, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, MvPolynomial.C_1, MvPolynomial.eval₂Hom_X', IsNonarchimedean.eval_mvPolynomial_le, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, ProjectiveSpectrum.as_ideal_le_as_ideal, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, wittPolynomial_one, MvPolynomial.pderiv_X, Algebra.FiniteType.baseChangeAux_surj, MvPolynomial.eval₂_mul_eq_zero_of_right, MvPolynomial.eval_eq', Algebra.Generators.H1Cotangent.δAux_toAlgHom, MvPolynomial.eval₂_C, Subalgebra.mvPolynomial_aeval_coe, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Algebra.Presentation.naive_relation_apply, Fin.accumulate_rec, MvPolynomial.C_add, PolynomialLaw.exists_lift, LinearMap.toMvPolynomial_zero, Multiset.toFinsupp_apply, MvPolynomial.isHomogeneous_C_mul_X, TensorPower.galgebra_toFun_def, WittVector.mul_polyOfInterest_aux4, Polynomial.coeff_mul, Multiset.cardHom_apply, 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_σ, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, MvPolynomial.mapAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, MvPolynomial.finitePresentation_universalFactorizationMap, ProjectiveSpectrum.as_ideal_lt_as_ideal, MvPolynomial.mapAlgEquiv_refl, WittVector.frobeniusPoly_zmod, MvPolynomial.eval_neg, Algebra.FiniteType.iff_quotient_mvPolynomial', IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, MvPolynomial.tensorEquivSum_one_tmul_C, ofAdd_mul, MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne, MvPolynomial.IsSymmetric.mul, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, WeierstrassCurve.Jacobian.baseChange_polynomialY, MonomialOrder.Monic.pow, MonomialOrder.degree_mul_of_isRegular_right, MvPolynomial.map_ofNat, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, MvPolynomial.coeff_monomial_mul, Polynomial.degree_freeMonic, MvPolynomial.IsWeightedHomogeneous.add, MvPolynomial.eval₂Hom_rename, MvPolynomial.degreeOf_pow_eq, ProjectiveSpectrum.mem_zeroLocus, LieModule.rank_eq_natTrailingDegree, MvPolynomial.bind₂_id, MvPolynomial.X_mul_cancel_left_iff, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier, MvPolynomial.sumAlgEquiv_comp_rename_inl, MvPolynomial.dvd_monomial_iff_exists, WeierstrassCurve.Projective.baseChange_polynomialY, AlgebraicIndependent.aeval_of_algebraicIndependent, MvPolynomial.aeval_bind₁, IsPrimitiveRoot.finite_quotient_span_sub_one', MonomialOrder.degree_sum_le, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, MvPolynomial.X_dvd_mul_iff, MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, MvPolynomial.algebraMap_apply, MvPolynomial.mkDerivationₗ_monomial, LieAlgebra.ad_pow_lie, MvPolynomial.killCompl_monomial_eq_zero_of_not_subset, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, MvPolynomial.exists_fin_rename, CategoryTheory.ShortComplex.ShortExact.extClass_naturality, LinearMap.toMvPolynomial_baseChange, MvPolynomial.optionEquivLeft_coeff_coeff, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, MvPowerSeries.truncFinset_C, Fin.accumulate_apply, MvPolynomial.C_surjective, MvPolynomial.pderiv_def, MvPolynomial.isEmptyRingEquiv_symm_apply, DFinsupp.toMultiset_le_toMultiset, MonomialOrder.degree_leadingTerm_mul, MvPolynomial.hom_eq_hom, ProjectiveSpectrum.gc_set, ceilRoot_def, IsPrimitiveRoot.finite_quotient_span_sub_one, MvPolynomial.mem_pow_idealOfVars_iff', MvPolynomial.mem_supported, Matrix.toMvPolynomial_zero, MvPolynomial.renameEquiv_apply, MvPolynomial.degrees_pow_le, MvPolynomial.rename_esymmAlgHom, MvPolynomial.aeval_eq_zero, MvPolynomial.eval₂_cast_comp, AddMonoidHom.ext_nat_iff, Algebra.PreSubmersivePresentation.naive_toPresentation, Polynomial.eval_homogenize, MvPolynomial.modMonomial_add_divMonomial, MonomialOrder.span_leadingTerm_eq_span_monomial', Finsupp.mem_toMultiset, MvPolynomial.bind₁_C_right, MvPolynomial.coe_coeffs_map, Polynomial.toTupleMvPolynomial_one_eq, MvPolynomial.rename_zero, AlgebraicGeometry.Proj.val_sectionInBasicOpen_apply, CategoryTheory.Abelian.Ext.comp_mk₀_id, MvPolynomial.instIsLocalHomRingHomAlgebraMap, WittVector.bind₁_wittMulN_wittPolynomial, PolynomialLaw.exists_range_φ_eq_of_fg, Algebra.FinitePresentation.mvPolynomial, MvPowerSeries.truncFinset_map, MvPolynomial.coeff_single_X_pow, MvPolynomial.dvd_X_mul_iff, MonomialOrder.degree_X_sub_C, MvPolynomial.monomial_one_mul_cancel_left_iff, MvPolynomial.eq_zero_iff, MvPolynomial.aevalTower_C, MvPolynomial.expand_one_apply, MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul, MvPolynomial.map_expand_pow_char, xInTermsOfW_aux, Finset.Nat.prod_antidiagonal_succ', Ring.descPochhammer_smeval_add, Algebra.Presentation.span_range_relation_eq_ker, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, MvPolynomial.mapRange_eq_map, MvPolynomial.monomial_mem_pow_idealOfVars_iff, MonomialOrder.degree_smul_le, MvPolynomial.irreducible_sumSMulX, AnalyticOnNhd.aeval_mvPolynomial, MvPolynomial.totalDegree_eq_zero_iff_eq_C, MvPowerSeries.coeff_expand_smul, Algebra.Generators.Hom.toAlgHom_X, MvPolynomial.bind₁_rename, MvPolynomial.degreeOf_sub_le, MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff, wittStructureRat_prop, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, MvPolynomial.degrees_rename, FreeMonoid.count_of, Algebra.Presentation.comp_relation, MvPolynomial.eval₂Hom_zero', Polynomial.Bivariate.equivMvPolynomial_symm_C, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', Algebra.Generators.instIsScalarTowerRing, MvPowerSeries.aeval_coe, MvPowerSeries.truncFinset_monomial_eq_zero, Multiset.coe_countPAddMonoidHom, MonomialOrder.toSyn_degree_mul_le, Polynomial.homogenize_X_pow, WittVector.IsPoly.poly, MvPolynomial.map_hsymm, Multiset.toDFinsupp_replicate, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, MvPolynomial.finite_universalFactorizationMap, MvPolynomial.rTensorAlgHom_toLinearMap, wittStructureRat_rec, CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc, WittVector.mul_polyOfInterest_vars, CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift, MvPolynomial.isRegular_prod_X, MvPolynomial.homogeneousSubmodule_zero, MvPolynomial.expand_eq_C, algebraicIndependent_iff, bell_succ', Multiset.uIcc_eq, MvPowerSeries.trunc'_expand, multiplesHom_symm_apply, MvPolynomial.universalFactorizationMapPresentation_map, MvPolynomial.coeff_rename_mapDomain, MonomialOrder.degree_mul_le, Finsupp.count_toMultiset, 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.degrees_map_le, MvPolynomial.esymmAlgHom_fin_surjective, MvPolynomial.expand_inj, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, MvPolynomial.coeff_prod_X_pow, MvPolynomial.supDegree_esymm, MvPolynomial.coeffsIn_mul, MvPolynomial.eval_eq, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, rothNumberNat_def, MvPowerSeries.rename_coe, MonomialOrder.sPolynomial_def, MvPolynomial.mk_eq_eval₂, Algebra.Generators.H1Cotangent.δAux_ofComp, MvPolynomial.restrictSupport_zero, bernoulli'_spec', MvPolynomial.killCompl_monomial_mapDomain, MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors, MonomialOrder.le_add_right, IsCyclotomicExtension.discr_prime_pow_ne_two, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, MvPolynomial.isUnit_iff_eq_C_of_isReduced, MvPolynomial.psum_zero, MvPolynomial.monomial_add_single, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, AddSubmonoid.fg_iff_exists_fin_addMonoidHom, MvPolynomial.le_coeffsIn_pow, MvPolynomial.supported_strictMono, MvPolynomial.IsWeightedHomogeneous.pow, MonomialOrder.degree_pow_le, MvPolynomial.eval_add, WeierstrassCurve.Projective.map_polynomialX, MvPolynomial.pointToPoint_zeroLocus_le, Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs, exists_integral_inj_algHom_of_quotient, MvPowerSeries.trunc_map, MvPolynomial.isNilpotent_iff, TensorAlgebra.ofDirectSum_toDirectSum, factorization_ceilRoot, Equiv.Perm.card_support_prod_list_of_pairwise_disjoint, AddMonoidHom.ENatMap_apply, MvPolynomial.instNoZeroDivisors, exists_finite_inj_algHom_of_fg, Polynomial.hasseDeriv_mul, MvPolynomial.zeroLocus_bot, WeierstrassCurve.Jacobian.baseChange_polynomial, MvPolynomial.aeval_def, MvPolynomial.monomial_eq_zero, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, MvPolynomial.eval_monomial, Finsupp.degree_preimage_add, Relation.cutExpand_le_invImage_lex, MonomialOrder.degree_C, List.ranges_flatten, MvPolynomial.coeff_monomial_mul', MonomialOrder.toSyn_monotone, MvPolynomial.degrees_sub_le, MvPolynomial.coe_eval₂Hom, MvPolynomial.vars_C_mul, MonomialOrder.sPolynomial_left_zero, AbsoluteValue.eval_mvPolynomial_le, Algebra.Generators.toAlgHom_ofComp_rename, Behrend.map_succ', Polynomial.toFinsupp_natCast, MonomialOrder.support_leadingTerm, Algebra.FinitePresentation.iff, DividedPowerAlgebra.dp_zero, wittStructureRat_rec_aux, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, MvPolynomial.eval₂_add, MonomialOrder.image_leadingTerm_insert_zero, WeierstrassCurve.Projective.eval_polynomialZ, MvPowerSeries.coeff_inv_aux, MvPolynomial.supported_mono, DFinsupp.toMultiset_toDFinsupp, Algebra.Generators.ker_localizationAway, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃, MonomialOrder.sPolynomial_decomposition, MonomialOrder.degLex_single_le_iff, MvPolynomial.constantCoeff_smul, MvPolynomial.totalDegree_expand, MvPolynomial.algHom_C, MvPolynomial.leadingCoeff_toLex_C, MvPolynomial.support_mul_X, wittStructureInt_prop, MvPolynomial.eval_pow, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, TensorPower.mul_one, MvPolynomial.eval₂Hom_zero'_apply, uliftMultiplesHom_apply_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, List.drop_sum_flatten, MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal, MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', MvPolynomial.mkₐ_eq_aeval, MvPolynomial.derivation_C, MvPolynomial.mem_support_coeff_optionEquivLeft, Algebra.Presentation.fg_ker, Height.mulHeight_eval_ge, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', instIsAlgebraicMvPolynomialOfNoZeroDivisors, Polynomial.eval_X_toTupleMvPolynomial_zero_eq, MvPolynomial.dvd_smul_X_iff_exists, MvPolynomial.mem_supported_vars, MvPolynomial.mkDerivation_monomial, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, Algebra.Presentation.relation_mem_ker, Algebra.Generators.Hom.toExtensionHom_toRingHom, MvPolynomial.schwartz_zippel_sup_sum, PolynomialModule.smul_apply, Algebra.Generators.comp_localizationAway_ker, CategoryTheory.ShortComplex.ShortExact.comp_extClass, MvPolynomial.mem_map_C_iff, MvPolynomial.rename_monomial, MvPolynomial.aeval_toMvPolynomial, Finset.Nat.sum_antidiagonal_swap, MvPolynomial.mul_esymm_eq_sum, MvPolynomial.prime_C_iff, MvPolynomial.eval_mul, MvPolynomial.restrictScalars_restrictSupportIdeal, MvPolynomial.degreesLE_zero, MvPolynomial.universalFactorizationMapPresentation_relation, MvPolynomial.aevalTower_comp_algebraMap, MvPolynomial.eval₂_zero_apply, Algebra.PreSubmersivePresentation.aevalDifferential_single, AlgebraicIndependent.algebraMap_aevalEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, MvPolynomial.isWeightedHomogeneous_zero, MonomialOrder.coeff_degree_eq_zero_iff, MvPolynomial.aeval_id_rename, Finsupp.toMultiset_add, Multiset.toFinsupp_singleton, MvPolynomial.degreeOf_mul_X_self, MonomialOrder.monic_C_one, MvPolynomial.eq_C_of_isEmpty, MonomialOrder.sPolynomial_right_zero, WeierstrassCurve.Projective.polynomialX_eq, Algebra.adjoin_range_eq_range_aeval, Multiset.toFinsupp_symm_apply, MvPolynomial.monomial_zero', MvPolynomial.eval₂_sub, Finset.sum_antidiagonal_choose_add, Algebra.Generators.aeval_val_σ, MvPolynomial.totalDegree_add, Polynomial.homogenize_C_mul, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', MvPolynomial.mem_zeroLocus_iff, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, MvPolynomial.coe_add, DFinsupp.toMultiset_inf, MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le, MvPolynomial.modMonomial_X, Finset.prod_antidiagonal_pow_choose_succ, MonomialOrder.leadingCoeff_add_of_lt, MvPolynomial.eval_indicator_apply_eq_zero, Multiset.replicateAddMonoidHom_apply, MvPolynomial.sumToIter_iterToSum, MvPolynomial.divMonomial_mul_monomial, MvPolynomial.map_surjective_iff, AlgebraicIndependent.eq_zero_of_aeval_eq_zero, roth_3ap_theorem_nat, constantCoeff_wittPolynomial, WeierstrassCurve.Projective.polynomialY_eq, MvPolynomial.aeval_eq_constantCoeff_of_vars, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, MvPolynomial.weightedHomogeneousComponent_finsupp, IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two, WeierstrassCurve.Projective.negDblY_eq, AlgebraicGeometry.Proj.zero_apply, powersHom_apply, SymmetricAlgebra.equivMvPolynomial_symm_X, MvPolynomial.coeff_linearCombination_X_pow, MvPolynomial.expand_bind₁, MvPolynomial.map_injective_iff, MvPolynomial.coeff_mul_X', MvPolynomial.prod_X_pow_eq_monomial, MvPolynomial.map_injective, MvPolynomial.constantCoeff_monomial, MvPolynomial.coeff_mul_X, MvPolynomial.smul_eval, ProjectiveSpectrum.vanishingIdeal_anti_mono, MvPolynomial.eval₂Hom_zero, MvPowerSeries.substAlgHom_coe, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, MvPolynomial.C_eq_zero, MvPolynomial.supDegree_toLex_C, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, MvPolynomial.coeff_rTensorAlgHom_tmul, MvPolynomial.aeval_zero, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', MvPolynomial.killCompl_rename_app, coe_castAddMonoidHom, powersMulHom_apply, MvPolynomial.hom_congr_vars, MvPolynomial.comp_aeval, Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk, MvPolynomial.support_map_of_injective, MvPolynomial.constantCoeff_X, MvPolynomial.frobenius_zmod, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous, 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, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, PowerSeries.coeff_mul, WeierstrassCurve.Projective.baseChange_polynomialX, Finset.Nat.prod_antidiagonal_subst, MvPolynomial.isLocalHom_expand, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne, MvPolynomial.C_mul', xInTermsOfW_vars_subset, AlgebraicClosure.le_maxIdeal, MvPolynomial.isEmptyAlgEquiv_apply, MvPolynomial.bind₂_X_right, MvPolynomial.of_irreducible_expand, Algebra.Generators.cMulXSubOneCotangent_eq, DividedPowerAlgebra.submodule_span_prod_dp_eq_top, MvPolynomial.map_C, LinearMap.polyCharpolyAux_baseChange, ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus, Polynomial.Bivariate.equivMvPolynomial_X, Finsupp.sum_antidiagonal_swap, MvPolynomial.C_dvd_iff_dvd_coeff, MvPolynomial.pderiv_C_mul, Module.Basis.symmetricAlgebra_repr_apply, MonomialOrder.degree_smul_of_isRegular, AlgebraicClosure.toSplittingField_coeff, CategoryTheory.Abelian.Ext.covariant_sequence_exact₂', MvPolynomial.eval₂_mul, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero, Matrix.toMvPolynomial_eval_eq_apply, MvPolynomial.coe_pow, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, MvPowerSeries.coeff_add_mul_monomial, MvPolynomial.natDegree_optionEquivLeft, Matrix.charpoly.univ_coeff_isHomogeneous, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, WittVector.constantCoeff_wittMul, MvPowerSeries.monomial_pow, Algebra.Generators.self_algebra_smul, MvPolynomial.restrictSupport_nsmul, MvPolynomial.mem_support_finSuccEquiv, List.sum_const_nat, CategoryTheory.Abelian.Ext.mono_postcomp_mk₀_of_mono, MvPolynomial.isNoetherianRing_fin, MvPolynomial.X_dvd_iff_modMonomial_eq_zero, Finsupp.coe_orderIsoMultiset_symm, MvPolynomial.funext_set_iff, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, MvPolynomial.X_mul_divMonomial, MvPolynomial.map_monomial, algebraicIndependent_iff_injective_aeval, MvPolynomial.vars_map_of_injective, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, MvPolynomial.rename_comp_toMvPolynomial, MvPolynomial.finSuccEquiv_comp_C_eq_C, MvPolynomial.esymmAlgHom_zero, MvPolynomial.homogeneousComponent_eq_zero, TensorAlgebra.toDirectSum_comp_ofDirectSum, MvPolynomial.coeToMvPowerSeries.algHom_apply, AlgebraicIndependent.liftAlgHom_comp_reprField, DividedPowerAlgebra.algHom_ext_iff, MvPolynomial.rename_rightInverse, char_dvd_card_solutions, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, WeierstrassCurve.Jacobian.polynomialZ_eq, MonomialOrder.sPolynomial_monomial_mul, MvPolynomial.eval₂Hom_map_hom, MvPolynomial.isRegular_X, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, MvPolynomial.finSuccEquiv_eq, char_dvd_card_solutions_of_sum_lt, SymmetricAlgebra.equivMvPolynomial_ι_apply, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, MvPolynomial.homogeneousComponent_zero, uliftPowersHom_apply_apply, LinearMap.polyCharpoly_eq_of_basis, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, MvPolynomial.bind₁_comp_rename, TensorPower.algebraMap₀_mul_algebraMap₀, MvPolynomial.coeff_map, MonomialOrder.degree_le_degree_of_support_subset, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, MvPolynomial.monomial_sum_index, LinearMap.polyCharpolyAux_map_aeval, Matrix.mvPolynomialX_mapMatrix_eval, MvPolynomial.monic_monomial_eq, MvPolynomial.image_support_finSuccEquiv, MvPolynomial.eval₂_rename, AlgebraicIndependent.aeval_repr, MvPolynomial.support_expand, AlgebraicGeometry.Proj.ext_iff, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, MonomialOrder.degree_eq_zero_iff, MvPolynomial.add_divMonomial, AddSubmonoid.one_eq_mrange, Polynomial.toFinsupp_algebraMap, Polynomial.Bivariate.equivMvPolynomial_C_X, Commute.add_pow', MvPolynomial.IsSymmetric.rename, MvPolynomial.IsHomogeneous.aeval, MvPolynomial.isEmptyRingEquiv_symm_toRingHom, AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen, MonomialOrder.leadingTerm_C, Finsupp.antidiagonal_zero, AddMonoidHom.apply_nat, WittVector.mul_polyOfInterest_aux1, MvPolynomial.monomial_mul, MonomialOrder.toSyn_eq_zero_iff, LieModule.toEnd_pow_lie, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, Height.mulHeight_eval_le, ProjectiveSpectrum.gc_ideal, MvPowerSeries.expand_monomial, MvPolynomial.aeval_bind₂, MvPolynomial.rename_bind₁, MvPolynomial.support_X_pow, MvPolynomial.pderiv_X_of_ne, MvPolynomial.prod_X_add_C_coeff, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, AlgebraicGeometry.Proj.add_apply, MvPolynomial.IsSymmetric.zero, Algebra.Generators.Hom.toAlgHom_comp_apply, MvPolynomial.degree_finSuccEquiv, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.isNoetherianRing_fin_0, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, MvPolynomial.nonempty_support_optionEquivLeft, MvPolynomial.isRegular_X_pow, ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure, bind₁_rename_expand_wittPolynomial, Algebra.adjoin_eq_range, MvPolynomial.degrees_add_le, MvPolynomial.mapAlgEquiv_symm, Algebra.Generators.toComp_toAlgHom_monomial, MvPolynomial.counit_surjective, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, DFinsupp.toMultiset_injective, MvPolynomial.rename_injective, Multiset.toFinsupp_zero, MvPolynomial.isHomogeneous_zero, Submodule.nat_power_gradedMonoid, MvPolynomial.degrees_mul_le, WeierstrassCurve.Projective.negDblY_eq', MvPolynomial.quotient_mk_comp_C_injective, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, AddSubmonoid.isLocalizationMap_top_nat_int, Multiset.toFinsupp_toMultiset, LinearMap.polyCharpolyAux_coeff_eval, MvPolynomial.esymmAlgHomMonomial_single_one, AlgebraicClosure.Monics.map_eq_prod, MvPolynomial.coe_smul, MonomialOrder.degree_prod_le, MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt, MvPolynomial.map_rightInverse, MvPolynomial.dvd_monomial_mul_iff_exists, MvPolynomial.killCompl_map, MonomialOrder.span_leadingTerm_insert_zero, Algebra.FiniteType.iff_quotient_mvPolynomial, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', MonomialOrder.div_set, MvPolynomial.aeval_eq_bind₁, MvPolynomial.support_optionEquivLeft, rootOfSplitsXPowSubC_pow, MvPolynomial.X_mul_modMonomial, MvPolynomial.degreeOf_pow_le, MvPolynomial.dvd_X_iff_exists, MvPolynomial.finSuccEquiv_X_succ, MvPolynomial.aeval_ofNat, List.headI_le_sum, MonomialOrder.degree_zero, Algebra.Presentation.aeval_val_relationOfHasCoeffs, MvPolynomial.eval₂Hom_eq_zero, MvPolynomial.instCharP, MvPolynomial.expand_comp_bind₁, MvPolynomial.mapAlgEquiv_trans, MonomialOrder.leadingCoeff_C, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, MvPolynomial.ker_mapAlgHom, Finsupp.degree_preimage_nsmul, MvPolynomial.aeval_injective_iff_of_isEmpty, tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm', WittVector.constantCoeff_wittAdd, Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp, Algebra.Generators.ofComp_kerCompPreimage, MvPolynomial.X_mem_supported, MvPolynomial.coeff_zero, MvPolynomial.eval_sub, MvPolynomial.esymmAlgHom_fin_injective, MvPolynomial.aeval_comp_bind₁, MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem, Height.logHeight_eval_le, List.sum_nat_mod, MvPolynomial.totalDegree_sub, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀, Polynomial.monic_freeMonic, MvPolynomial.eval₂_const_pUnitAlgEquiv, Algebra.Generators.repr_CotangentSpaceMap, DividedPowerAlgebra.dp_sum_smul, MonomialOrder.degLex_lt_iff, MvPolynomial.pderiv_pow, constantCoeff_wittStructureRat_zero, WeierstrassCurve.Jacobian.map_polynomialZ, DividedPowers.OfInvertibleFactorial.dpow_add_of_lt, MvPolynomial.aeval_esymm_eq_multiset_esymm, MvPolynomial.supported_le_supported_iff, MvPolynomial.totalDegree_zero, MonomialOrder.coeff_pow_nsmul_degree, MvPolynomial.bind₂_C_right, MvPolynomial.constantCoeff_eq, LinearMap.toMvPolynomial_constantCoeff, WeierstrassCurve.Projective.map_polynomialZ, MvPolynomial.eval_rename, MvPolynomial.mkDerivationₗ_C, CategoryTheory.InjectiveResolution.mk₀_comp_extMk, StandardEtalePresentation.toPresentation_σ', factorization_eq_primeFactorsList_multiset, CategoryTheory.Abelian.Ext.mono_precomp_mk₀_of_epi, MvPolynomial.isIntegral_iff_isIntegral_coeff, witt_structure_prop, factorization_floorRoot, MvPolynomial.map_surjective, MvPolynomial.coe_eval₂AlgHom, WittVector.constantCoeff_wittNSMul, LinearMap.toMvPolynomial_comp, PowerSeries.coeff_inv, ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal, floorRoot_def, 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, TruncatedWittVector.card_zmod, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card, MvPolynomial.eval₂_map_comp_C, MonomialOrder.degree_pow, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, MvPolynomial.vanishingIdeal_empty, MvPolynomial.C_eq_coe_nat, MvPolynomial.tensorEquivSum_X_tmul_X, MvPolynomial.comp_aeval_apply, MvPolynomial.vars_mul, Algebra.Presentation.relation_comp_localizationAway_inl, MvPolynomial.bind₂_comp_bind₂, WittVector.coeff_select, Finsupp.toFinset_toMultiset, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, MvPolynomial.aeval_unique, WeierstrassCurve.Jacobian.baseChange_polynomialX, DividedPowerAlgebra.dp_def, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, MvPolynomial.bind₁_bind₁, PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2, MvPolynomial.degreeOf_mul_C_le, MvPolynomial.esymmAlgHomMonomial_add, MvPolynomial.algebraTensorAlgEquiv_symm_map, MvPolynomial.coeff_sub, MvPolynomial.rename_polynomial_aeval_X, MvPolynomial.degrees_mul_eq, MvPolynomial.coeff_expand_of_not_dvd, DividedPowerAlgebra.dp_sum, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, MvPolynomial.isHomogeneous_C_mul_X_pow, ProjectiveSpectrum.basicOpen_eq_union_of_projection, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus, MvPolynomial.tensorEquivSum_C_tmul_one, addSubmonoid_fg, MvPolynomial.map_iterateFrobenius_expand, MvPolynomial.vars_pow, Polynomial.toMvPolynomial_X, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, MvPolynomial.sumAlgEquiv_apply, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, cyclotomicCharacter.toFun_apply, Multiset.toFinsupp_eq_iff, Algebra.Generators.ker_comp_eq_sup, MvPolynomial.degreeOf_C_mul_le, quadraticChar_odd_prime, algebraicIndependent_subtype, LinearMap.polyCharpoly_map_eq_charpoly, MonomialOrder.degree_add_eq_right_of_lt, AlgebraicGeometry.stalkToFiberRingHom_germ, MvPolynomial.sumToIter_Xr, LinearMap.polyCharpoly_monic, Polynomial.natDegree_freeMonic, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, MvPolynomial.exists_finset_rename₂, Matrix.charpoly.univ_natDegree, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, MvPolynomial.algebraMap_eq, MvPolynomial.eval_toMvPolynomial, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, Algebra.Generators.aeval_val_eq_zero, MvPolynomial.coeffsIn_pow, MvPolynomial.sum_C, cyclotomicCharacter.toZModPow_toFun, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, MvPolynomial.esymmAlgHom_apply, MvPolynomial.monomial_eq, MvPolynomial.aeval_eq_eval₂Hom, MvPolynomial.vars_C, MvPolynomial.rename_prod_mk_eval₂, AlgebraicIndependent.aevalEquivField_apply_coe, MvPolynomial.IsSymmetric.smul, MvPolynomial.aeval_C, MvPolynomial.support_map_subset, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀, ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPolynomial.transcendental_polynomial_aeval_X, MvPolynomial.pderiv_map, WeierstrassCurve.Jacobian.eval_polynomial, MvPowerSeries.coeff_invOfUnit, MvPolynomial.aeval_comp_expand, Algebra.Generators.naive_σ, AlgebraicIndependent.aevalEquiv_apply_coe, Polynomial.homogenize_monomial_of_lt, WittVector.wittMul_zero, MvPolynomial.rename_C, Finsupp.toMultiset_sum, MvPolynomial.HomogeneousSubmodule.gradedMonoid, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, legendreSym.card_sqrts, MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc', TensorPower.one_mul, Multiset.toDFinsupp_injective, MvPolynomial.eval₂_mul_C, MonomialOrder.degree_lt_of_left_ne_zero_of_degree_mul_lt, StandardEtalePresentation.aeval_val_equivMvPolynomial, Submonoid.mem_closure_finset, MvPolynomial.C_neg, MvPolynomial.weightedHomogeneousComponent_eq_zero, MvPolynomial.aevalTower_comp_toAlgHom, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, MvPolynomial.coeToMvPowerSeries.ringHom_apply, fib_succ_eq_sum_choose, MvPolynomial.restrictSupport_add, MvPolynomial.eval₂_X_pow, MvPolynomial.zeroLocus_span, MvPolynomial.instIsCancelMulZeroOfIsCancelAdd, MvPolynomial.coeffs_map, MvPolynomial.IsHomogeneous.rename_isHomogeneous, WittVector.polyOfInterest_vars_eq, ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal, WeierstrassCurve.Jacobian.map_polynomial, MvPolynomial.mapEquiv_trans, MvPolynomial.isNoetherianRing, MvPolynomial.constantCoeff_comp_C, MvPolynomial.pderiv_inr_universalFactorizationMap_X, MvPolynomial.degrees_zero, MvPolynomial.IsHomogeneous.mul, MvPolynomial.sumAlgEquiv_symm_apply, MvPolynomial.eval₂_comp, TensorAlgebra.equivDirectSum_symm_apply, MvPolynomial.weightedHomogeneousComponent_C_mul, MonomialOrder.leadingCoeff_zero, MvPolynomial.eval₂_pUnitAlgEquiv_symm, CategoryTheory.Abelian.Ext.postcomp_mk₀_injective_of_mono, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, MvPolynomial.dvd_C_iff_exists, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Generators.ker_ofAlgHom, MvPolynomial.mul_monomial_mem_coeffsIn, Multiset.toDFinsupp_le_toDFinsupp, MvPolynomial.supported_empty, MvPolynomial.C_mem_pow_idealOfVars_iff, Multiset.toDFinsupp_toMultiset, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, KaehlerDifferential.mvPolynomialBasis_repr_D, MonomialOrder.sPolynomial_monomial_mul', MvPolynomial.pderiv_eq_zero_of_notMem_vars, Multiset.toDFinsupp_singleton, WittVector.map_frobeniusPoly, Finset.Nat.antidiagonal_filter_le_fst_of_le, MvPolynomial.sum_eval_eq_zero, MvPolynomial.support_divMonomial, MvPolynomial.le_degrees_add_right, MvPolynomial.weightedTotalDegree'_zero, WittVector.constantCoeff_wittZSMul, WeierstrassCurve.Jacobian.polynomialX_eq, MvPolynomial.aeval_C_comp_left, MvPolynomial.transcendental_X, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.totalDegree_mul, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, AlgebraicGeometry.Proj.stalkIso'_germ, MvPolynomial.degrees_rename_of_injective, PolynomialLaw.range_φ, MvPolynomial.coeff_add, MvPolynomial.psum_eq_mul_esymm_sub_sum, Polynomial.toFinsuppIsoAlg_apply, List.mem_mem_ranges_iff_lt_sum, MvPolynomial.eval_C, MvPolynomial.IsWeightedHomogeneous.C_mul, MvPolynomial.mapAlgHom_apply, MvPolynomial.support_zero, Algebra.Generators.cotangentRestrict_mk, MvPolynomial.optionEquivLeft_monomial, MonoidHom.ext_mnat_iff, MvPolynomial.rename_eq_zero_iff_of_injective, Algebra.Generators.H1Cotangent.δ_eq_δAux, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, MonomialOrder.leadingCoeff_mul_of_isRegular_left, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, LieAlgebra.rank_eq_natTrailingDegree, WittVector.bind₁_onePoly_wittPolynomial, Polynomial.toFinsupp_sub, map_wittPolynomial, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, Finset.Nat.antidiagonal_filter_snd_le_of_le, MvPolynomial.isLocalization_C_mk', Behrend.map_zero, MvPolynomial.algebraTensorAlgEquiv_tmul, MvPolynomial.vars_map, MvPolynomial.mem_support_coeff_finSuccEquiv, Algebra.Generators.aeval_val_σ', MvPolynomial.support_sub, Algebra.Generators.Hom.toAlgHom_id, Algebra.Generators.Hom.comp_val, MvPolynomial.degreeOf_C_mul, xInTermsOfW_vars_aux, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, MvPolynomial.C_injective, MvPolynomial.C_mul, Multiset.coe_countAddMonoidHom, MvPolynomial.comap_apply, ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal, MvPolynomial.vars_rename, MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars, WittVector.bind₁_zero_wittPolynomial, ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem, List.length_sigma, MonomialOrder.lex_lt_iff, MvPolynomial.isLocalization, MvPolynomial.instExpChar, MvPolynomial.divMonomial_monomial_mul, StandardEtalePresentation.toPresentation_val, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, MvPolynomial.instIsCancelAddOfIsLeftCancelAdd, MvPolynomial.rename_comp_bind₁, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.mem_basicOpen_den, MvPolynomial.degrees_monomial_eq, MvPolynomial.zeroLocus_top, MvPolynomial.aeval_id_eq_join₁, MvPolynomial.rename_X, MvPolynomial.IsSymmetric.C, MvPolynomial.pUnitAlgEquiv_monomial, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, MvPolynomial.coeff_mul_monomial, Polynomial.homogenize_sub, MvPolynomial.degreeOf_zero, MvPolynomial.ringHom_ext'_iff, MvPolynomial.mem_ideal_span_monomial_image_iff_dvd, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero, IsRegular.monomial, Matrix.charpoly.univ_map_eval₂Hom, summable_sum_mul_antidiagonal_of_summable_norm', MvPolynomial.comap_id_apply, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂, MvPolynomial.aeval_one_tmul, MvPolynomial.monomial_pow, Finsupp.prod_antidiagonal_swap, MvPolynomial.divMonomial_add_modMonomial_single, MvPolynomial.eval_sum, MvPolynomial.degreeOf_sub_lt, MvPolynomial.smul_eq_C_mul, MvPolynomial.counitNat_C, TensorPower.mul_algebraMap₀, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, Algebra.Presentation.HasCoeffs.relation_mem_range_map, MvPolynomial.rename_expand, Polynomial.ofFinsupp_zsmul, 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.IsHomogeneous.sum_X_mul_pderiv, MvPolynomial.derivation_C_mul, MvPolynomial.aeval_sumElim_pderiv_inl, MvPolynomial.monomial_one_dvd_monomial_one, CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc, AnalyticAt.aeval_mvPolynomial, MvPolynomial.mul_monomial_modMonomial, ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus, MvPolynomial.eval₂_natCast, MvPolynomial.tensorEquivSum_one_tmul_X, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis, AddMonoid.instFGNat, MvPolynomial.iterToSum_C_C, MvPolynomial.mapEquiv_refl, MvPolynomial.totalDegree_sub_C_le, MvPolynomial.coeffAddMonoidHom_apply, MvPolynomial.coeff_X_mul, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, MvPolynomial.supported_univ, ProjectiveSpectrum.mem_coe_basicOpen, MvPolynomial.isSymmetric_rename, MvPolynomial.eval₂_C_mk_eq_zero, MvPolynomial.universalFactorizationMap_freeMonic, Algebra.Generators.Hom.toAlgHom_monomial, Polynomial.homogenize_zero, MvPolynomial.le_degrees_add_left, MonomialOrder.sPolynomial_mem_ideal, MvPolynomial.mem_ideal_of_coeff_mem_ideal, MvPolynomial.irreducible_of_totalDegree_eq_one, MvPolynomial.universalFactorizationMapPresentation_val, catalan_succ', MvPolynomial.rename_comp_rename, MonomialOrder.leadingCoeff_sub_of_lt, MvPolynomial.coe_expand, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, MvPolynomial.aeval_sumElim, MvPolynomial.universalFactorizationMapPresentation_σ', analyticOrderNatAt_pow, Multiset.toDFinsupp_inter, MvPolynomial.aeval_comp_rename, LinearMap.toMvPolynomial_eval_eq_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, MvPolynomial.mem_symmetricSubalgebra, MonomialOrder.degree_mul_of_isRegular_left, autEquivRootsOfUnity_apply_rootOfSplit, Behrend.map_eq_iff, MvPolynomial.support_rename_killCompl_subset, factorization_pow, 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, MvPolynomial.schwartz_zippel_sum_degreeOf, MvPolynomial.isHomogeneous_C, Algebra.FinitePresentation.out, List.take_sum_flatten, MvPolynomial.rename_leftInverse, MonomialOrder.Monic.mul, ax_grothendieck_of_locally_finite, Algebra.FiniteType.iff_quotient_mvPolynomial'', Algebra.Presentation.quotientEquiv_mk, Finsupp.toMultiset_single, MvPolynomial.esymmAlgHom_fin_bijective, toAdd_pow, Behrend.threeAPFree_image_sphere, MvPolynomial.esymmAlgEquiv_apply, Polynomial.homogenize_C, MvPolynomial.eval₂AlgHom_X, MvPolynomial.mem_vanishingIdeal_iff, MonomialOrder.degree_add_of_lt, MvPolynomial.mem_vanishingIdeal_singleton_iff, MonomialOrder.div, FreeAddMonoid.countP_apply, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃', MvPolynomial.weightedTotalDegree'_eq_bot_iff, WittVector.mul_polyOfInterest_aux5, Multiset.toDFinsupp_lt_toDFinsupp, MvPolynomial.expand_zmod, MonomialOrder.lex_le_iff, MvPolynomial.aeval_zero', Multiset.toDFinsupp_union, MvPolynomial.weightedTotalDegree_rename_of_injective, AlgebraicGeometry.ProjectiveSpectrum.comapFun_asHomogeneousIdeal, MvPolynomial.range_mapAlgHom, MvPolynomial.counit_C, MvPolynomial.weightedHomogeneousComponent_of_mem, WeierstrassCurve.Projective.baseChange_polynomialZ, MvPolynomial.irreducible_sumSMulXSMulY, ceilDiv_eq_add_pred_div, IsPrimitiveRoot.zeta_sub_one_prime, MvPolynomial.counitNat_X, MonomialOrder.degree_sPolynomial_le, MonomialOrder.degree_X_add_C, MvPolynomial.eval₂Hom_bind₂, MvPolynomial.mem_ideal_span_monomial_image, MvPolynomial.rename_toMvPolynomial, MvPolynomial.aeval_rename, addRothNumber_Ico, MonomialOrder.Monic.add_of_lt, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, MvPolynomial.optionEquivLeft_symm_C_X, MvPolynomial.mul_X_modMonomial, MvPolynomial.bind₂_bind₂, WittVector.aeval_verschiebungPoly, MvPolynomial.eval₂Hom_bind₁, Polynomial.homogenize_X, MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.degreeOf_eq_natDegree, MvPowerSeries.support_expand_subset, WeierstrassCurve.Projective.dblX_eq, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply, MonomialOrder.coeff_mul_of_degree_add, Finset.Nat.antidiagonal_eq_map', Algebra.Presentation.baseChange_relation, MonomialOrder.degree_sub_leadingTerm_lt_degree, MonomialOrder.sPolynomial_mem_sup_ideal, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁, ax_grothendieck_univ, MvPolynomial.C_mem_coeffsIn, summable_norm_sum_mul_antidiagonal_of_summable_norm, MvPolynomial.bind₁_X_right, MvPolynomial.coeff_rename_eq_zero, MvPowerSeries.monomial_mul_monomial, MonomialOrder.coeff_mul_of_add_of_degree_le, Polynomial.degree_pow', TensorPower.toTensorAlgebra_galgebra_toFun, MvPolynomial.join₂_map, MvPolynomial.eval₂Hom_C_left, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, MvPolynomial.aeval_monomial, CategoryTheory.Abelian.Ext.covariant_sequence_exact₂, Polynomial.homogenize_eq_zero_iff, StandardEtalePresentation.toPresentation_relation, DividedPowerAlgebra.dp_smul, Polynomial.toMvPolynomial_injective, IsCyclotomicExtension.Rat.discr_odd_prime', Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, TensorAlgebra.toDirectSum_ι, Finset.Nat.antidiagonal_filter_fst_le_of_le, MvPolynomial.coeff_eval_eq_eval_coeff, MvPolynomial.C_pow, LinearMap.polyCharpoly_natDegree, MvPolynomial.coeffs_C_subset, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, MvPolynomial.IsSymmetric.add, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing, MonomialOrder.degree_mul, MonomialOrder.degree_monomial_le, MvPolynomial.C_sub, Algebra.Generators.self_algebra_algebraMap, Finsupp.toMultiset_sup, MvPolynomial.coeff_mul_monomial', DFinsupp.toMultiset_inj, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, WittVector.mul_polyOfInterest_aux3, WittVector.verschiebungPoly_zero, MvPolynomial.pderiv_C, MonomialOrder.degLex_single_lt_iff, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, MvPolynomial.modMonomial_add_divMonomial_single, constantCoeff_xInTermsOfW, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, MvPolynomial.C_dvd_iff_zmod, MvRatFunc.rank_eq_max_lift, MvPolynomial.aeval_prod, MvPolynomial.homogeneousSubmodule_mul, Matrix.toMvPolynomial_mul, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, WittVector.wittOne_pos_eq_zero, Height.mulHeight_eval_le', List.sum_map_count_dedup_filter_eq_countP, MvPowerSeries.trunc_C_mul, MvPolynomial.exists_restrict_to_vars, wittStructureInt_rename, WittVector.constantCoeff_wittNeg, algebraicIndependent_comp_subtype, map_wittStructureInt, MvPolynomial.algebraTensorAlgEquiv_symm_monomial, MonomialOrder.degree_sub_LTerm_lt, MvPolynomial.constantCoeff_comp_map, Finsupp.sub_single_one_add, FreeMonoid.countP_apply, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, MvPolynomial.vars_add_subset, MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq, MvPolynomial.aevalTower_algebraMap, MvPolynomial.optionEquivLeft_elim_eval, Finset.Nat.antidiagonal_filter_le_snd_of_le, MvPolynomial.optionEquivLeft_symm_X, MvPolynomial.renameEquiv_symm, TensorAlgebra.ofDirectSum_comp_toDirectSum, MvPolynomial.eval₂Hom_C, DFinsupp.toMultiset_lt_toMultiset, MvPolynomial.counitNat_surjective, FreeMonoid.count_apply, MvPolynomial.support_symmDiff_support_subset_support_add, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, MvPolynomial.sumToIter_C, Height.mulHeight_eval_ge', WeierstrassCurve.Projective.dblX_eq', MvPolynomial.eval_expand, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, FreeAddMonoid.countP_of, MvPolynomial.aeval_comp_toMvPolynomial, AlgebraicGeometry.Proj.res_apply, MvPolynomial.divMonomial_add, MvPolynomial.supportedEquivMvPolynomial_symm_C, Polynomial.toFinsupp_intCast, Matrix.toMvPolynomial_constantCoeff, MvPowerSeries.trunc'_map, MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset, MvPolynomial.eval₂AlgHom_apply, MvPolynomial.tensorEquivSum_X_tmul_one, MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet, MvPolynomial.C_inj, MvPolynomial.expand_mul_eq_comp, WeierstrassCurve.Jacobian.map_polynomialY, MvPolynomial.eval₂_pUnitAlgEquiv, MvPolynomial.eval_X, Ideal.mem_span_pow_iff_exists_isHomogeneous, MvPolynomial.killCompl_monomial, one_mem_closure_iff, Polynomial.map_map_freeMonic, Partition.coeff_genFun, MvPolynomial.supported_eq_range_rename, WeierstrassCurve.Projective.dblY_of_Y_eq', MvPolynomial.IsHomogeneous.C_mul, MvPolynomial.rename_hsymm, MonomialOrder.sPolynomial_decomposition', MvPolynomial.constantCoeff_map, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, ProbabilityTheory.Kernel.partialTraj_zero, MvPolynomial.transcendental_supported_X, MvPolynomial.degrees_add_of_disjoint, DividedPowerAlgebra.dp_add, MvPolynomial.aeval_natDegree_le, AnalyticOnNhd.eval_continuousLinearMap', HomogeneousLocalization.Away.finiteType, MvPolynomial.optionEquivLeft_symm_C_C, MvPowerSeries.le_lexOrder_mul, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, Algebra.Generators.Hom.algebraMap_toAlgHom, MvPolynomial.IsSymmetric.sub, powersMulHom_symm_apply, MonomialOrder.C_mul_leadingCoeff_monomial_degree, WittVector.coeff_frobenius, ChevalleyThm.MvPolynomialC.numBound_casesOn_succ, MvPolynomial.degreeOf_mul_X_of_ne, Finset.Nat.sum_antidiagonal_succ, Finsupp.nsmul_single_one_image, Function.locallyFinsuppWithin.single_pos_nat_one, Algebra.Generators.comp_σ, AnalyticOnNhd.eval_mvPolynomial, MvPowerSeries.monomial_smul_eq, DividedPowerAlgebra.dp_null_of_ne_zero, WeierstrassCurve.Projective.map_polynomialY, MvPolynomial.tensorEquivSum_C_tmul_C, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, AlgebraicGeometry.Proj.stalkIso'_symm_mk, WeierstrassCurve.Projective.map_polynomial, WittVector.wittSub_zero, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', DividedPowerAlgebra.mkRingHom_C, MvPolynomial.instIsDomainOfIsCancelAdd, MvPowerSeries.subst_coe, MvPolynomial.mapEquivMonic_symm_map_algebraMap, WittVector.wittZero_eq_zero, MvPolynomial.coe_aeval_eq_eval, Finsupp.toMultiset_sum_single, WeierstrassCurve.Projective.eval_polynomialY, Multiset.toFinsupp_support, DividedPowerAlgebra.prod_dp, exists_integral_inj_algHom_of_fg, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso, MvPowerSeries.coeff_mul_of_add_lexOrder, MvPolynomial.instIsLocalHomRingHomC, MvPolynomial.eval₂_eq_eval_map, MvPolynomial.coeff_add_pow, multiplesHom_apply, Finsupp.toMultiset_map, MvPolynomial.weightedTotalDegree_zero, Matrix.charpoly.univ_coeff_card, Polynomial.Bivariate.equivMvPolynomial_C_C, MonomialOrder.degree_sub_of_lt, DividedPowerAlgebra.mkAlgHom_C, MvPolynomial.isWeightedHomogeneous_C, Polynomial.ofFinsupp_nsmul, MvPolynomial.map_X, ProjectiveSpectrum.coe_vanishingIdeal, MvPolynomial.eval_assoc, MvPolynomial.monomial_single_add, ax_grothendieck_zeroLocus, wittPolynomial_eq_sum_C_mul_X_pow, add_choose_eq, Polynomial.homogenize_one, MvPolynomial.support_X_mul, MvPolynomial.coeffs_zero, MvPolynomial.monomial_one_mul_cancel_right_iff, MonomialOrder.degree_mul', constantCoeff_wittStructureInt_zero, Algebra.Generators.ker_naive, factorization_mul_of_coprime, Multiset.toFinsupp_strictMono, Polynomial.homogenize_mul, MonomialOrder.degree_sPolynomial_lt_sup_degree, MonomialOrder.leadingTerm_eq_zero_iff, instFreeMvPolynomialKaehlerDifferential, MvPolynomial.hom_bind₁, WeierstrassCurve.Jacobian.map_polynomialX, MvPolynomial.coeff_expand_zero, MvPolynomial.C_dvd_iff_map_hom_eq_zero, Finsupp.toMultiset_inf, rank_mvPolynomial_mvPolynomial, AnalyticOnNhd.eval_continuousLinearMap, FirstOrder.Language.BoundedFormula.relabel_sumInl, WeierstrassCurve.Jacobian.eval_polynomialZ, Finset.Nat.antidiagonalEquivFin_apply_val, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, MvPolynomial.degreeOf_add_le, Matrix.mvPolynomialX_mapMatrix_aeval, Submonoid.mem_closure_iff_exists_finset_subset, MvPolynomial.algebraMap_def, MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero, MvPolynomial.support_C, MvPolynomial.supported_eq_vars_subset, MvPolynomial.coeffs_X_mul, Behrend.threeAPFree_sphere, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, DividedPowerAlgebra.embed_def, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective, MonomialOrder.degree_sub_leadingTerm_lt_iff, MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm, MvPolynomial.eval₂_comp_right, Polynomial.aeval_homogenize_of_eq_one, Finsupp.coe_orderIsoMultiset, MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors, MvPolynomial.map_eval, MonomialOrder.degree_sub_leadingTerm_le, Polynomial.homogenize_dvd, MvPolynomial.rename_eq, MvPolynomial.totalDegree_coeff_optionEquivLeft_le, MvPolynomial.coeff_mul, MvPolynomial.eval₂Hom_smul, WittVector.wittAdd_zero, MvPolynomial.mapEquivMonic_symm_map, MvPolynomial.mem_ideal_span_X_image, char_dvd_card_solutions_of_fintype_sum_lt, MvPolynomial.vars_0, MvPolynomial.isHomogeneous_X_pow, MvPolynomial.vars_add_of_disjoint, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bind₁_monomial, LinearMap.polyCharpoly_coeff_eval, tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm, Polynomial.ofFinsupp_intCast, MonomialOrder.degree_smul_of_mem_nonZeroDivisors, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, Multiset.toDFinsupp_inj, MvPolynomial.coe_mul, ProjectiveSpectrum.vanishingIdeal_union, MvPolynomial.continuous_eval, Algebra.Presentation.mem_ker_naive, MvPolynomial.C_eq_smul_one, MvPowerSeries.coeff_mul, MvPolynomial.coeff_killCompl, MvPolynomial.evalₗ_apply, List.headI_add_tail_sum, MvPolynomial.esymmAlgHom_surjective, MvPolynomial.aevalTower_ofNat, MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range, MvPolynomial.monomial_modMonomial, MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid, Finset.Nat.antidiagonal_succ', MvPolynomial.esymmAlgEquiv_symm_apply, MvPowerSeries.lexOrder_mul_ge, instIsPushoutFractionRingMvPolynomial_1, MvPolynomial.rename_surjective, Finsupp.toMultiset_eq_iff, Fin.accumulate_injective, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', MvPolynomial.map_id, IsCyclotomicExtension.discr_prime_pow, MvPowerSeries.coeff_add_monomial_mul, MvPolynomial.eval₂Hom_comp_expand, Polynomial.toMvPolynomial_C, MonomialOrder.degree_sub_LTerm_le, MonomialOrder.lex_le_iff_of_unique, MonomialOrder.sPolynomial_mul_monomial, Fin.accumulate_last, CategoryTheory.ShortComplex.ShortExact.extClass_comp, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two, MvPowerSeries.trunc'_C, ProjectiveSpectrum.vanishingIdeal_univ, MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero, List.drop_take_succ_flatten_eq_getElem, Algebra.Generators.Hom.equivAlgHom_apply_coe, Algebra.Generators.C_mul_X_sub_one_mem_ker, IsPrimitiveRoot.zeta_sub_one_prime', MvPolynomial.universalFactorizationMapPresentation_jacobian, Behrend.map_monotone, DividedPowerAlgebra.dp_eq_mkRingHom, MonomialOrder.sPolynomial_leadingTerm_mul, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, isLinearSet_iff_exists_fin_addMonoidHom, MvPolynomial.esymmAlgHom_injective, MvPowerSeries.trunc'_C_mul, MvPolynomial.commAlgEquiv_C_X, MvPolynomial.expand_zero_apply, Finset.nsmul_piAntidiag_univ, IsCyclotomicExtension.discr_prime_pow_ne_two', WeierstrassCurve.Projective.negDblY_of_Y_eq', Polynomial.coeff_freeMonic, MonomialOrder.degree_sPolynomial, CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zero, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', MvPolynomial.renameSymmetricSubalgebra_apply_coe, Algebra.FinitePresentation.iff_quotient_mvPolynomial', IsPrimitiveRoot.toInteger_sub_one_not_dvd_two, Finset.Nat.sum_antidiagonal_succ', MvPolynomial.monomial_dvd_monomial, MonomialOrder.degree_X_le_single, MvPolynomial.coe_mapEquivMonic_comp, MvPolynomial.eq_zero_of_eval_zero_at_prod_finset, MvPolynomial.transcendental_supported_polynomial_aeval_X, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom, instIsPushoutFractionRingMvPolynomial, Height.max_mulHeightBound_zero_one_eq_one, MvPolynomial.monomial_mul_modMonomial, MvPolynomial.eval_polynomial_eval_finSuccEquiv, MvPolynomial.constantCoeff_comp_algebraMap, MvPolynomial.sumToIter_Xl, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, DividedPowerAlgebra.dp_null, MvPolynomial.pderiv_inl_universalFactorizationMap_X, WittVector.constantCoeff_wittSub, Finset.nsmul_piAntidiag, MvPolynomial.counit_X, MvPolynomial.instFaithfulSMul, MvPolynomial.rename_id, MvPolynomial.eval₂Hom_comp_C, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, MvPolynomial.idealOfVars_fg, MvPolynomial.rTensorAlgHom_apply_eq
instAddSemigroup 📖	CompOp	2 math math: TensorPower.mul_assoc, FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe
instCommMonoid 📖	CompOp	195 math math: Fintype.card_pi, coe_properDivisors_eq_prod_pow_lt_factorization, smoothNumbersUpTo_subset_image, Finset.card_pi, prod_primeFactors_sdiff_of_squarefree, Finsupp.card_Ioc, factorization_prod_pow_eq_self_of_le_factorization, factorization_prod_pow_eq_self, coprime_multiset_prod_right_iff, Finsupp.card_Ico, ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors, ArithmeticFunction.cardFactors_multiset_prod, Pi.card_Ici, Equiv.Perm.card_of_cycleType_mul_eq, mem_finMulAntidiag, factors_multiset_prod_of_irreducible, coe_divisors_eq_prod_pow_le_factorization, prod_range_factorial_succ, Multiset.card_pi, Multiset.card_Ico, prod_pow_pos_of_zero_notMem_support, Pi.card_Iic, Equiv.Perm.OnCycleFactors.kerParam_range_card, ModEq.prod, Fintype.card_filter_piFinset_eq, prod_factorial_pos, eq_prod_primes_mul_sq_of_mem_smoothNumbers, AddSubgroup.index_iInf_le, prod_primeFactors_of_squarefree, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, Finset.card_dfinsupp, coprime_fintype_prod_left_iff, ModEq.multisetProd_map, prod_primeFactors_dvd, Polynomial.card_eq_of_natDegree_le_of_coeff_le, Matrix.card_GL_field, finPiFinEquiv_apply, prod_fermatNumber, primorial_add, factorization_prod_apply, properDivisors_eq_image_Iio_factorization_prod_pow, AddSubgroup.index_pi, ModEq.prod_one, radical_eq_prod_primeFactors, Multiset.card_Ioc, Ideal.iInf_span_singleton_natCast, Pi.card_Ioc, Multiset.bell_mul_eq, Pi.card_Icc, ArithmeticFunction.IsMultiplicative.map_prod_of_prime, Polynomial.ncard_boxPoly, Fintype.card_piFinset, Equiv.Perm.card_isConj_eq, DFinsupp.card_Iic, Pi.card_uIcc, eq_factorization_iff, Finsupp.card_Icc, Multiset.prod_nat_mod, IsCyclotomicExtension.Rat.discr, cast_finprod, Multiset.card_uIcc, Finsupp.card_uIcc, Subgroup.index_iInf_le, Finsupp.card_Ioo, ceilRoot_def, Pi.card_Iio, Equiv.Perm.card_of_cycleType, DFinsupp.card_Ioo, divisors_eq_map_attach_Iic_factorization_prod_pow, instIsMulTorsionFree, ArithmeticFunction.cardDistinctFactors_prod, chineseRemainderOfMultiset_lt_prod, cast_prod, prod_factorial_dvd_factorial_sum, coprime_multiset_prod_left_iff, prod_Icc_factorial, ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul, Polynomial.Chebyshev.iterate_derivative_U_eval_one_dvd, prod_pow_dvd_of_le_factorization, AlternatingGroup.card_of_cycleType, prod_pow_prime_padicValNat, Polynomial.Chebyshev.iterate_derivative_T_eval_one_dvd, Fintype.card_filter_piFinset_eq_of_mem, Finset.nat_divisors_prod, Finset.prod_Ico_id_eq_factorial, uniformBell_eq, Finset.lcm_eq_prod, Finset.prod_range_add_one_eq_factorial, sum_divisors_filter_squarefree, Prime.dvd_finsuppProd_iff, multinomial_spec, Choose.lucas_theorem_nat, Subgroup.index_pi, DFinsupp.card_uIcc, ascFactorial_eq_prod_range, DomMulAct.stabilizer_card', dvd_iff_exists_le_factorization, Choose.choose_modEq_choose_mul_prod_range_choose, card_divisors, IsCyclotomicExtension.Rat.natAbs_discr, ModEq.multisetProd_map_one, Finsupp.card_pi, Coprime.prod_right, Pi.card_Ico, Subgroup.relIndex_iInf_le, Iio_factorization_prod_pow_injective, Prime.not_dvd_finsuppProd, cast_finsuppProd, DFinsupp.card_pi, cast_multiset_prod, descFactorial_eq_prod_range, prod_pow_primeFactors_factorization, Finset.prod_range_natCast_sub, superFactorial_two_mul, prod_modEq_ite, prod_eq_of_mem_finMulAntidiag, Multiset.nat_divisors_prod, Polynomial.Chebyshev.iterate_derivative_U_eval_one, Multiset.bell_eq, prod_pow_factorization_eq_self, doubleFactorial_eq_prod_odd, floorRoot_def, prod_factorization_pow_eq_self, dvd_prod_pow_of_factorization_le, ArithmeticFunction.carmichael_finset_prod, card_pi, DFinsupp.card_Ico, factorizationEquiv_symm_apply_coe, totient_eq_prod_factorization, ArithmeticFunction.IsMultiplicative.map_prod, centralBinom_factorization_small, prod_pow_factorization_choose, sum_divisors, Int.radical_eq_prod_primeFactors, Finsupp.card_Iic, chineseRemainderOfFinset_lt_prod, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, finPiFinEquiv_single, Finsupp.card_Iio, factorizationEquiv_inv_apply, Coprime.prod_left, Multiset.card_Iic, Polynomial.Chebyshev.iterate_derivative_U_eval_one_eq_div, Polynomial.Chebyshev.iterate_derivative_T_eval_one, Multiset.card_sections, coprime_prod_left_iff, ENat.toNat_prod, doubleFactorial_eq_prod_even, Multiset.card_Icc, Finset.prod_natCast, properDivisors_eq_map_attach_Iio_factorization_prod_pow, prod_primeFactors_invOn_squarefree, superFactorial_four_mul, cast_finprod_mem, fermatNumber_eq_prod_add_two, PrimeMultiset.prod_ofNatMultiset, prod_modEq_single, DomMulAct.stabilizer_ncard, divisors_filter_squarefree, Finset.prod_nat_mod, prod_pow_factorization_centralBinom, Finset.PNat.coe_prod, totient_eq_div_primeFactors_mul, primeFactors_prod, DFinsupp.card_Iio, Choose.choose_modEq_prod_range_choose_nat, Multiset.card_Ioo, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite, DFinsupp.card_Icc, DomMulAct.stabilizer_card, coprime_fintype_prod_right_iff, factorial_eq_prod_range_add_one, factorization_prod, AddSubgroup.relIndex_iInf_le, Polynomial.Chebyshev.iterate_derivative_T_eval_one_eq_div, PrimeMultiset.coe_prod, AlternatingGroup.card_of_cycleType_mul_eq, finMulAntidiag_eq_piFinset_divisors_filter, Pi.card_Ioo, Pi.card_Ioi, Equiv.Perm.card_isConj_mul_eq, Equiv.Perm.nat_card_centralizer, prime_pow_pow_totient_ediv_prod, DFinsupp.card_Ioc, Finset.card_finsupp, Polynomial.card_mahlerMeasure_le_prod, prod_primeFactors_pow_totient_ediv_dvd, cast_finprod', ModEq.multisetProd_one, Iic_factorization_prod_pow_injective, totient_mul_prod_primeFactors, card_linearIndependent, prod_range_succ_factorial, coprime_prod_right_iff, divisors_eq_image_Iic_factorization_prod_pow
instCommSemigroup 📖	CompOp	—
instMonoid 📖	CompOp	959 math math: squarefree_and_prime_pow_iff_prime, pow_expChar_pow_inj_of_pNilradical_eq_bot, exists_eq_pow_of_exponent_coprime_of_pow_eq_pow, Behrend.sum_lt, pow_sub_one_gcd_pow_sub_one, ofDigits_eq_sum_mapIdx_aux, ack_add_one_sq_lt_ack_add_three, Prime.emultiplicity_choose_prime_pow_add_emultiplicity, mem_properDivisors_prime_pow, ZMod.isCyclic_units_iff_of_odd, Finset.addEnergy_eq_sum_sq', Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex, wittPolynomial_zmod_self, coe_properDivisors_eq_prod_pow_lt_factorization, Prime.exists_orderOf_eq_pow_factorization_exponent, smoothNumbersUpTo_subset_image, multiplicity_eq_factorization, IsPurelyInseparable.minpoly_natDegree_eq', bijOn_digitsAppend', PadicInt.lift_sub_val_mem_span, LucasLehmer.X.card_eq, Int.natCast_multiplicity, sub_pow_expChar_pow_of_commute, IsPrimePow.exists_ordCompl_eq_one, Subgroup.index_center_le_pow, padicValNat_dvd_iff_of_ne_one, IsPGroup.card_center_eq_prime_pow, TruncatedWittVector.card, IsPurelyInseparable.minpoly_eq', IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow, BitVec.equivFin_symm_apply_toFin, dvd_sub_pow_of_dvd_sub, NNRat.num_pow, ArithmeticFunction.cardFactors_pow, factorization_prod_pow_eq_self_of_le_factorization, ordCompl_le, ChevalleyThm.MvPolynomialC.degBound_casesOn_succ, ofDigits_lt_base_pow_length, multiplicative_factorization', SModEq.pow_pow_add_one, add_pow_expChar_pow_of_commute, IsPrimePow.minFac_pow_factorization_eq, IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable', WittVector.toZModPow_compat, sq_mul_squarefree_of_pos, factorization_prod_pow_eq_self, WeierstrassCurve.coeff_preΨ', JacobsonNoether.exists_pow_mem_center_of_inseparable', IsPurelyInseparable.elemExponent_min', PreTilt.valAux_eq, IsLowerSet.le_card_inter_finset, divisors_filter_squarefree_of_squarefree, sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, padicValNat.maxPowDiv_eq_multiplicity, ArithmeticFunction.carmichael_pow_of_prime_ne_two, ZMod.orderOf_one_add_mul_prime, toNat_emultiplicity, add_pow_char_pow, aeval_wittPolynomial, ChevalleyThm.chevalley_polynomialC, divisors_prime_pow, PadicInt.zmod_congr_of_sub_mem_span, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, WittVector.map_frobeniusPoly.key₂, sq_mul_squarefree, SzemerediRegularity.a_add_one_le_four_pow_parts_card, pow, getD_digits, sub_dvd_pow_sub_pow, pow_succ_padicValNat_not_dvd, Primrec.pow, List.card_fixedLengthDigits, WittVector.RecursionMain.succNthVal_spec', Irreducible.natSepDegree_eq_one_iff_of_monic', Polynomial.rootMultiplicity_expand_pow, SzemerediRegularity.card_chunk, IsPRadical.pow_mem, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, uniformBell_eq_div, coe_divisors_eq_prod_pow_le_factorization, cyclotomicCharacter.toZModPow, Sylow.exists_subgroup_card_pow_prime_of_le_card, IsPurelyInseparable.elemExponent_min, Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible', add_pow_prime_pow_eq, IsPurelyInseparable.elemExponent_def', LiouvilleNumber.partialSum_eq_rat, exists_base_eq_prime_pow_of_prime_pow_eq_base_pow, ZMod.unitsMap_self, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, IsPurelyInseparable.hasExponent_iff, ExpChar.pow_prime_pow_mul_eq_one_iff, padicValNat.pow_two_sub_one_ge, Prime.mul_eq_prime_sq_iff, prod_pow_pos_of_zero_notMem_support, ordCompl_dvd_ordCompl_iff_dvd, Finset.sum_condensed_le, NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow, IsPurelyInseparable.finrank_eq_pow, ordProj_of_not_prime, ArithmeticFunction.cardDistinctFactors_apply_prime_pow, Finset.mulEnergy_univ_left, IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two, Finset.mulEnergy_univ_right, Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, pow_succ_factorization_not_dvd, pow_pow_modEq_one, Odd.nat_add_dvd_pow_add_pow, Behrend.sum_sq_le_of_mem_box, WeierstrassCurve.natDegree_ΨSq, Prime.factorization_pow, Dynamics.IsDynCoverOf.iterate_le_pow, iterateFrobeniusEquiv_def, Finset.card_Ioo_finset, Choose.choose_pow_mul_pow_mul_modEq_choose, four_pow_le_two_mul_self_mul_centralBinom, card_dvd_exponent_pow_rank, summable_condensed_iff_of_eventually_nonneg, jacobiSym.pow_right, Behrend.bound_aux', ArithmeticFunction.sigma_apply, Prime.primeFactorsList_pow, add_pow_expChar_pow, Behrend.map_succ, Ideal.absNorm_eq_pow_inertiaDeg', Behrend.le_N, Behrend.map_le_of_mem_box, squarefree_of_factorization_le_one, Finset.card_pow_le, ofDigits_lt_base_pow_length', choose_succ_le_two_pow, GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible, ArithmeticFunction.sigma_one_apply_prime_pow, Fintype.card_piFinset_const, BitVec.ofFin_intCast, eq_prod_primes_mul_sq_of_mem_smoothNumbers, factorization_factorial, SimpleGraph.farFromTriangleFree_iff, Prime.emultiplicity_factorial, padicValNat_dvd_iff, Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap, Char.card_pow_char_pow, pow_card_sub_one_sub_one_mod_card, mem_rootsOfUnity_prime_pow_mul_iff', Ico_pow_dvd_eq_Ico_of_lt, IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable, IsLowerSet.card_inter_le_finset, eq_sq_add_sq_iff_eq_sq_mul, ArithmeticFunction.moebius_sq, sum_pow_char_pow, coprime_pow_right_iff, BoxIntegral.Prepartition.card_filter_mem_Icc_le, ZMod.isCyclic_units_iff, Prime.dvd_choose_pow, ordCompl_div_of_dvd, DirichletCharacter.zetaMul_prime_pow_nonneg, uniformBell_mul_eq, IsPurelyInseparable.iterateFrobenius_algebraMap, Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, ofDigits_eq_sum_mapIdx, primeFactors_pow_succ, IteratedWreathProduct.card, exists_add_pow_prime_pow_eq, Fintype.sum_piFinset_apply, Finset.le_sum_condensed', IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, Polynomial.rootsExpandPowEquivRoots_apply, RegularWreathProduct.card, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, squarefree_pow_iff, modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, totient_prime_pow, ordCompl_dvd_ordCompl_of_dvd, FiniteField.pow_card_pow, Finset.geomSum_le_geomSum_iff_toColex_le_toColex, LinearIndependent.map_pow_expChar_pow_of_isSeparable', Prime.emultiplicity_le_emultiplicity_choose_add, Int.exists_sq_add_sq_add_one_eq_mul, IsCyclotomicExtension.Rat.discr_prime_pow', IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, ArithmeticFunction.moebius_apply_prime_pow, eventually_pow_lt_factorial_sub, Int.ofNat_isUnit, AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul, ofDigits_digits_append_digits, geomSum_lt, sum_range_choose, ZMod.val_pow_le, IsCyclotomicExtension.Rat.absdiscr_prime_pow, two_pow_and, ofDigits_mod_pow_eq_ofDigits_take, padicValNat_prime_prime_pow, IsPGroup.iff_card, WeierstrassCurve.coeff_preΨ, Equiv.Perm.VectorsProdEqOne.card, pow_length_le_mul_ofDigits, two_pow_sub_pow, Choose.lucas_theorem, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow, factorization_eq_card_pow_dvd_of_lt, Sylow.prime_pow_dvd_card_normalizer, Prime.emultiplicity_factorial_mul, Fintype.card_set, BoundingSieve.prodPrimes_squarefree, PadicInt.ext_of_toZModPow, EulerProduct.eulerProduct_hasProd, Finset.addEnergy_univ_left, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two, fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq, FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard, FiniteField.algebraMap_trace_eq_sum_pow, Choose.choose_modEq_prod_range_choose, Polynomial.roots_X_pow_char_pow_sub_C_pow, exists_eq_pow_of_pow_eq_pow, ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Finset.addEnergy_eq_sum_sq, choose_lt_two_pow, primorial_le_four_pow, Matrix.card_GL_field, ordProj_dvd_ordProj_iff_dvd, Mathlib.Tactic.Ring.coeff_mul, pow_mul_mem_smoothNumbers, IsPurelyInseparable.minpoly_eq, factoredNumbers.map_prime_pow_mul, dvd_pow_pow_sub_self_of_dvd, ArithmeticFunction.IsMultiplicative.eulerProduct_hasProd, Finset.mulEnergy_eq_sum_sq', FiniteField.exists_forall_apply_eq_pow, ordCompl_pow_mul_eq_self_iff, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, emultiplicity_pow_prime_pow_sub_pow_prime_pow, tsum_eq_tsum_primes_of_support_subset_prime_powers, xInTermsOfW_eq, EulerProduct.eulerProduct, sub_pow_char_pow_of_commute, CommGroup.coe_primaryComponent, IsLowerSet.le_card_inter_finset', mem_perfectClosure_iff_pow_mem, LinearMap.iterateFrobenius_def, multiset_sum_pow_char_pow, factorization_choose_prime_pow_add_factorization, IsPGroup.exists_card_eq, four_pow_le_two_mul_add_one_mul_central_binom, JacobsonNoether.exists_pow_mem_center_of_inseparable, LucasLehmer.sZMod_eq_sMod, bijOn_ofDigits, Choose.choose_pow_mul_pow_mul_modEq_choose_nat, sub_mem_pNilradical_iff_pow_expChar_pow_eq, Commute.exists_add_pow_prime_pow_eq, Int.emultiplicity_pow_sub_pow, Fintype.card_pi_const, ModEq.pow_card_sub_one_eq_one, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, SimpleGraph.farFromTriangleFree.le_card_sub_card, ZMod.natCast_pow_eq_zero_of_le, Finset.card_Iio_finset, emultiplicity_pow_add_pow, powMulEquiv_pow, properDivisors_eq_image_Iio_factorization_prod_pow, Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval, composition_card, ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totient, Ordinal.natCast_opow, exists_pow_eq_iff', Commute.add_pow_prime_pow_eq, irreducible_iff_prime, units_eq_one, choose_middle_le_pow, BoundingSieve.squarefree_of_dvd_prodPrimes, primorial_lt_four_pow, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero, isPrimePow_nat_iff, pow_sub_one_dvd_pow_sub_one, DividedPowers.dpow_prod, IsPurelyInseparable.HasExponent.has_exponent, selfAdjoint.nnnorm_pow_two_pow, eq_prime_pow_of_dvd_least_prime_pow, AddCommGroup.equiv_free_prod_directSum_zmod, ArithmeticFunction.sigma_apply_prime_pow, Ideal.index_pow_le, Chebyshev.sum_PrimePow_eq_sum_sum, padicValNat.pow_sub_pow, WeierstrassCurve.natDegree_Φ_le, Behrend.map_apply, ordProj_mul_ordCompl_eq_self, pairwise_coprime_pow_primeFactors_factorization, Configuration.ProjectivePlane.card_points, Finset.geomSum_ofColex_strictMono, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two, Prime.emultiplicity_choose', euler_four_squares, Finset.le_card_mul_mul_mulEnergy, X_pow_sub_C_irreducible_iff_of_prime_pow, Field.span_map_pow_expChar_pow_eq_top_of_isSeparable, IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two, EulerProduct.eulerProduct_tprod, SeparableClosure.hasEnoughRootsOfUnity_pow, Polynomial.rootsExpandPowToRoots_apply, isPurelyInseparable_iff_pow_mem, Finset.card_Icc_finset, exists_pow_eq_iff, padicValNat.pow, padicValNat_choose', NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, card_vector, Finset.lt_geomSum_of_mem, Prime.pow_dvd_factorial_iff, WeierstrassCurve.natDegree_ΨSq_le, ofDigits_div_pow_eq_ofDigits_drop, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub, bijOn_ofDigits', FiniteField.pow_finrank_eq_natCard, exists_addOrderOf_eq_prime_pow_iff, dvd_ordCompl_of_dvd_not_dvd, Primes.prodNatEquiv_apply, ArithmeticFunction.carmichael_two_pow_of_le_two, eq_factorization_iff, ArithmeticFunction.IsMultiplicative.eulerProduct_tprod, AddCommGroup.equiv_directSum_zmod_of_finite, isPrimePow_nat_iff_bounded, Prime.not_prime_pow', ack_three, append_lt, ArithmeticFunction.sigma_le_pow_succ, IsCyclotomicExtension.Rat.discr, cast_npow, properDivisors_prime_pow, EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers, LucasLehmer.X.card_units_lt, IsUpperSet.le_card_inter_finset, Pell.xy_modEq_yn, Prime.emultiplicity_choose, ceilRoot_def, IsPrimitiveRoot.finite_quotient_span_sub_one, Int.two_pow_two_pow_add_two_pow_two_pow, finInsepDegree_eq_pow, Finset.toFinset_bitIndices_twoPowSum, LucasLehmer.ω_pow_eq_one, AddCommMonoid.coe_primaryComponent, TruncatedWittVector.commutes_symm', FiniteField.algebraMap_norm_eq_prod_pow, Sylow.exists_subgroup_card_pow_prime_le, Polynomial.cyclotomic_prime_pow_eq_geom_sum, Polynomial.HasSeparableContraction.dvd_degree', Mathlib.Tactic.Ring.natCast_mul, Mathlib.Tactic.Ring.mul_exp_pos, Module.card_eq_pow_finrank, digits_append_digits, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, LucasLehmer.X.closed_form, WeierstrassCurve.coeff_Φ, sub_one_dvd_pow_sub_one, two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq, mem_perfectClosure_iff, probablePrime_iff_modEq, IsPurelyInseparable.exponent_def', MvPolynomial.map_expand_pow_char, xInTermsOfW_aux, emultiplicity_two_factorial_lt, bertrand_main_inequality, ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient, sum_four_squares, pow_dvd_iff_dvd_floorRoot, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', pred_mul_geom_sum_le, Polynomial.natSepDegree_X_pow_char_pow_sub_C, eq_sq_add_sq_iff, lt_pow_nthRoot_add_one, ModN.natCard_eq, Finset.equivBitIndices_symm_apply, wittStructureRat_rec, divisors_eq_map_attach_Iic_factorization_prod_pow, FiniteField.isSplittingField_of_nat_card_eq, four_pow_lt_mul_centralBinom, IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ, Set.ncard_powerset, orderOf_eq_prime_pow, IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero, IsPGroup.nontrivial_iff_card, TruncatedWittVector.charP_zmod, Irreducible.natSepDegree_eq_one_iff_of_monic, IsPGroup.card_orbit, IsSelfAdjoint.norm_pow_two_pow, ordCompl_pow_mul_of_not_dvd, even_pow', Subgroup.card_commutator_dvd_index_center_pow, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, Int.natCast_emultiplicity, MulChar.IsQuadratic.gaussSum_frob_iter, not_dvd_ordCompl, CircleDeg1Lift.transnumAuxSeq_def, ZMod.castHom_self, IsCyclotomicExtension.discr_prime_pow_ne_two, Polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one, FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate, Polynomial.smeval_at_natCast, Finset.card_Ico_finset, IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two, IsCyclotomicExtension.Rat.discr_prime_pow_succ, eq_pow_of_factorization_eq_single, Perfection.teichmullerFun_sModEq, Perfection.teichmuller_sModEq, WeierstrassCurve.natDegree_Φ, mapsTo_digitsAppend, Finpartition.card_atomise_le, ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul, nthRoot_pow, pow_nthRoot_le_iff, Perfection.teichmuller₀_sModEq, LucasLehmer.sZMod_eq_s, wittStructureRat_rec_aux, Fintype.card_finset, Polynomial.eval_one_cyclotomic_prime_pow, prod_pow_dvd_of_le_factorization, Module.natCard_eq_pow_finrank, prod_pow_prime_padicValNat, padicValNat.pow_add_pow, multiplicity_choose_aux, geomSum_eq, WittVector.iterate_frobenius_coeff, Prime.emultiplicity_self, isPrimePow_nat_iff_bounded_log, Dioph.pow_dioph, two_mul_sq_add_one_le_two_pow_two_mul, ModEq.pow_totient, even_pow, iterateFrobenius_def, PadicInt.zmod_cast_comp_toZModPow, Int.shiftLeft_eq_mul_pow, Prime.emultiplicity_choose_prime_pow, NNRat.den_pow, Finset.card_sq_le_card_mul_mulEnergy, Fintype.card_filter_piFinset_const_eq_of_mem, Finset.card_filter_length_eq_le, mul_le_pow, emultiplicity_eq_ofNat, succ_mersenne, ArithmeticFunction.IsMultiplicative.eulerProduct, card_dvd_exponent_pow_rank', ArithmeticFunction.moebius_ne_zero_iff_squarefree, PNat.Coprime.pow, padicValNat_def, Perfection.coeffMonoidHom_pow_p_pow', EulerProduct.prod_filter_prime_tsum_eq_tsum_factoredNumbers, Polynomial.roots_expand_pow_map_iterateFrobenius_le, IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem, Polynomial.Monic.natSepDegree_eq_one_iff, sum_divisors_filter_squarefree, odd_pow_iff, card_fun, tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers, setOf_pow_dvd_eq_Icc_factorization, Finset.le_sum_condensed, ZMod.isCyclic_units_of_prime_pow, lt_base_pow_length_digits', base_pow_length_digits_le', Sylow.exists_subgroup_le_card_pow_prime_of_le_card, smoothNumbersUpTo_card_le, card_dvd_exponent_nsmul_rank, Int.squarefree_natAbs, factorization_choose', Ordinal.natCast_pow, cardQuot_pow_of_prime, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, Int.natCast_pow_pred, Sylow.exists_subgroup_card_pow_prime, Primes.coe_prodNatEquiv_apply, add_pow_char_pow_of_commute, prod_divisors_prime_pow, exists_orderOf_eq_prime_pow_iff, ZMod.orderOf_one_add_four_mul, ArithmeticFunction.sigma_zero_apply_prime_pow, fib_two_mul_add_one, padicNorm.dvd_iff_norm_le, Polynomial.exists_approx_polynomial, Choose.lucas_theorem_nat, AddMonoid.End.natCast_def, EulerProduct.eulerProduct_hasProd_mulIndicator, twoPowSum_bitIndices, sub_pow_char_pow, CommGroup.equiv_free_prod_prod_multiplicative_zmod, PadicInt.toZModPow_eq_iff_ext, AbsoluteValue.IsAdmissible.exists_approx, Icc_factorization_eq_pow_dvd, ordCompl_pos, padicValNat.prime_pow, WittVector.frobeniusPolyAux_eq, PadicInt.fwdDiff_iter_le_of_forall_le, ordCompl_mul, Polynomial.natDegree_iterate_comp, ordProj_le, Multiset.card_antidiagonal, dvd_iff_exists_le_factorization, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, ENNReal.tsum_condensed_le, Polynomial.cyclotomic_mul_prime_pow_eq, equivProdNatSmoothNumbers_apply', Choose.choose_modEq_choose_mul_prod_range_choose, IsCyclotomicExtension.Rat.natAbs_discr, FiniteField.isSplittingField_of_card_eq, cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, Pell.eq_pow_of_pell_lem, centralBinom_le_four_pow, digits_length_le_iff, Finset.le_card_add_mul_addEnergy, ordProj_dvd_ordProj_of_dvd, pow_sub_one_mod_pow_sub_one, ofDigits_reverse_cons, Polynomial.natSepDegree_expand, FiniteField.card, Sylow.card_eq_multiplicity, Finset.card_sq_le_card_mul_addEnergy, AddCommGroup.coe_primaryComponent, IsPurelyInseparable.minpoly_natDegree_eq, iterate_frobenius, nthRoot.lt_pow_go_succ_aux, Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs, IsPurelyInseparable.algebraMap_elemReduct_eq', Iio_factorization_prod_pow_injective, Ring.smeval_ascPochhammer_nat_cast, nthRoot_lt_iff, sum_range_choose_sq, Projectivization.card_of_finrank, pow_mul_mem_factoredNumbers, Behrend.card_sphere_le_rothNumberNat, IsPurelyInseparable.algebraMap_iterateFrobenius, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, fermat_primeFactors_one_lt, ordCompl_self_pow_mul, IsPrimitiveRoot.norm_pow_sub_one_two, squarefree_iff_nodup_primeFactorsList, equivProdNatFactoredNumbers_apply, PadicInt.ker_toZModPow, WeierstrassCurve.natDegree_preΨ_le, isUnit_iff, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, padicValNat_choose, WittVector.mul_polyOfInterest_aux1, dvd_pow_iff_ceilRoot_dvd, ack_add_one_sq_lt_ack_add_four, neg_one_pow_char_pow, IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable', padicValNat_factorial, Polynomial.roots_expand_pow_map_iterateFrobenius, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, Polynomial.map_expand_pow_char, compositionAsSet_card, pow_pow_add_primeFactors_one_lt, prod_properDivisors_prime_pow, multinomial_two_mul_le_mul_multinomial, setInvOn_digitsAppend_ofDigits, IsCyclotomicExtension.Rat.discr_prime_pow, BoundingSieve.squarefree_of_mem_divisors_prodPrimes, prod_pow_primeFactors_factorization, ZMod.orderOf_one_add_prime, FiniteField.natCard_extension, MvPowerSeries.map_iterateFrobenius_expand, iterate_frobeniusEquiv_symm_pow_p_pow, superFactorial_two_mul, Int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul, Finset.card_biUnion_le_of_intersecting, IsSepClosed.hasEnoughRootsOfUnity_pow, eight_dvd_sq_sub_one_of_odd, mem_pNilradical, Finpartition.card_filter_atomise_le_two_pow, padicValRat.multiplicity_sub_multiplicity, list_sum_pow_char_pow, Int.emultiplicity_pow_add_pow, BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le, ChevalleyThm.MvPolynomialC.degBound_succ, expChar_pow_pos, padicValNat.div_pow, pow_left_strictMono, ordProj_self_pow, exists_ordCompl_eq_one_iff_isPrimePow, Finset.mulEnergy_eq_sum_sq, LucasLehmer.order_ω, ProbabilityTheory.Fernique.measure_gt_normThreshold_le_rpow, ENNReal.le_tsum_condensed, Prime.pow_dvd_iff_dvd_ordProj, padicValNat_def', prod_pow_factorization_eq_self, pow_totient_mod_eq_one, lt_digits_length_iff, ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers, summable_condensed_iff_of_nonneg, ordCompl_div_pow_of_dvd, FiniteField.pow_finrank_eq_card, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, choose_lt_pow, WeierstrassCurve.natDegree_preΨ', LinearIndependent.map_pow_expChar_pow_of_isSeparable, Matrix.toLinearMap₂'_single, WittVector.iterate_verschiebung_mul_coeff, floorRoot_def, TruncatedWittVector.card_zmod, centralBinom_lt_four_pow, IsPurelyInseparable.pow_mem, add_pow_prime_pow_eq', prod_factorization_pow_eq_self, ZMod.orderOf_one_add_mul_prime_pow, sum_divisors_prime_pow, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, dvd_prod_pow_of_factorization_le, Int.squarefree_natCast, VectorSpace.card_fintype, IsPGroup.index, Finset.twoPowSum_toFinset_bitIndices, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, Finset.card_Ioc_finset, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, MvPolynomial.map_iterateFrobenius_expand, padicValNat_dvd_iff_le_of_ne_one, cyclotomicCharacter.toFun_apply, WittVector.nth_mul_coeff, ofDigits_append, cyclotomicCharacter.toZModPow_toFun, succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul, factorizationEquiv_symm_apply_coe, totient_eq_prod_factorization, Prime.emultiplicity_pow, ZMod.castHom_bijective, eventually_mul_pow_lt_factorial_sub, Int.emultiplicity_natAbs, eq_sq_add_sq_of_isSquare_mod_neg_one, TruncatedWittVector.zmodEquivTrunc_apply, centralBinom_factorization_small, Multiset.card_powerset, prod_pow_factorization_choose, Prime.not_prime_pow, minpoly.natSepDegree_eq_one_iff_pow_mem, LucasLehmer.norm_num_ext.sModNat_eq_sMod, Prime.emultiplicity_factorial_le_div_pred, Finset.card_Iic_finset, Prime.sq_add_sq, sum_divisors, Ico_filter_pow_dvd_eq, PNat.pow_coe, factorization_pow_self, Finset.le_mulEnergy_self, GaloisField.card, padicValNat_eq_emultiplicity_of_ne_one, Prime.pow_minFac, PadicInt.lift_spec, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, EulerProduct.one_sub_inv_eq_geometric_of_summable_norm, geom_sum_le, Besicovitch.card_le_of_separated, and_two_pow, PreTilt.untilt_iterate_frobeniusEquiv_symm_pow, tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers, Behrend.card_box, IsPurelyInseparable.exponent_min, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum, nat_log_eq_padicValNat_iff, padicValNat.pow_two_sub_pow, X_pow_sub_C_irreducible_of_prime_pow, exists_eq_pow_mul_and_not_dvd, factorization_eq_card_pow_dvd, PadicInt.zmod_congr_of_sub_mem_span_aux, Prime.multiplicity_factorial_pow, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, ZMod.pow_card_pow, LucasLehmer.ω_pow_eq_neg_one, IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow, cyclotomicCharacter.spec, sub_one_mul_sum_div_pow_eq_sub_sum_digits, Rat.mkRat_pow, Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible, factorization_ordCompl, multiplicative_factorization, pow_add_mul_totient_mod_eq, primeFactors_pow, DirichletCharacter.changeLevel_self_toUnitHom, pow_sub_pow_dvd_pow_sub_pow, Prime.emultiplicity_one, factorizationEquiv_inv_apply, WeierstrassCurve.natDegree_preΨ'_le, Perfection.coeffMonoidHom_pow_p_pow_self, AbsoluteValue.IsAdmissible.exists_approx_aux, Int.coe_nat_two_pow_pred, charP_of_prime_pow_injective, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, Fintype.card_finsupp, ArithmeticFunction.pow_apply, Polynomial.exists_separable_of_irreducible, squarefree_two, Polynomial.roots_expand_image_iterateFrobenius, ZMod.orderOf_five, IsPurelyInseparable.hasExponent_iff', nat_repr_len_aux, ordProj_dvd, SimpleGraph.regularityReduced_edges_card_aux, bijOn_digitsAppend, pow_minFac, SzemerediRegularity.card_aux₂, hyperoperation_three, Module.card_fintype, Prime.emultiplicity_mul, FiniteField.X_pow_card_pow_sub_X_natDegree_eq, isReduced_zmod, doubleFactorial_two_mul, Polynomial.roots_expand_pow_image_iterateFrobenius_subset, Behrend.bound_aux, squarefree_iff_minSqFac, modEq_mersenne, coprime_pow_primes, Ideal.absNorm_eq_pow_inertiaDeg, coprime_ordCompl, Int.two_pow_two_pow_sub_pow_two_pow, Configuration.ProjectivePlane.card_lines, dvd_iff_prime_pow_dvd_dvd, Prime.pow_dvd_iff_le_factorization, totient_prime_pow_succ, TruncatedWittVector.commutes, ZMod.castHom_injective, ZMod.val_pow, pow_nthRoot_le, equivProdNatFactoredNumbers_apply', IsCyclotomicExtension.Rat.ramificationIdx_eq, map_prime_pow_mul, Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow, Prime.divisors_sq, isPrimePow_nat_iff_bounded_log_minFac, mem_divisors_prime_pow, SimpleGraph.triangle_removal, FiniteField.card', sum_sum_digits_eq, squarefree_iff_prime_squarefree, Fintype.card_filter_piFinset_const, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, Sylow.exists_subgroup_card_pow_succ, Prime.deficient_pow, Polynomial.roots_expand_pow, Besicovitch.multiplicity_le, pow_of_pow_add_prime, IsCyclotomicExtension.norm_zeta_pow_sub_one_two, sum_range_mul_choose, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, IsPurelyInseparable.exponent_min', IsPGroup.iff_orderOf, LucasLehmer.ω_pow_formula, IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap, dvd_ordProj_of_dvd, SimpleGraph.card_edgeFinset_turanGraph, factorization_pow, properDivisors_eq_map_attach_Iio_factorization_prod_pow, ordProj_pos, pow_totient_mod, cast_pow, ordCompl_eq_self_iff_zero_or_not_dvd, shiftLeft_lt, primorial_le_4_pow, SimpleGraph.card_edgeFinset_completeEquipartiteGraph, WittVector.map_frobeniusPoly.key₁, Polynomial.eval₂_one_cyclotomic_prime_pow, DistribSMul.toAddMonoidHom_eq_nsmulAddMonoidHom, prod_primeFactors_invOn_squarefree, ordProj_mul, Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP, superFactorial_four_mul, floorRoot_pow_self, CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow, IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap_base, lt_base_pow_length_digits, finFunctionFinEquiv_apply_val, ZMod.isCyclic_units_two_pow_iff, eq_two_pow_or_exists_odd_prime_and_dvd, eq_prime_pow_of_unique_prime_dvd, le_nthRoot_iff, sq_add_sq_modEq, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, padicValNat_mul_pow_left, pow_add_totient_mod_eq, Prime.emultiplicity_factorial_mul_succ, factorization_choose_prime_pow, irreducible_iff_nat_prime, IsPurelyInseparable.algebraMap_elemReduct_eq, Function.minimalPeriod_eq_prime_pow, IsPrimitiveRoot.zeta_sub_one_prime, self_mod_pow_eq_ofDigits_take, ArithmeticFunction.carmichael_factorization, emultiplicity_pow_sub_pow, factorization_choose, IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable, WittVector.teichmuller_mul_pow_coeff, padicValNat.pow_two_sub_one, sum_range_choose_halfway, floorRoot_pow_dvd, Finset.card_nsmul_le, replicate_subperm_primeFactorsList_iff, card_dvd_exponent_nsmul_rank', Subalgebra.mem_perfectClosure_iff, padicValNat_dvd_iff_le, ceilRoot_pow_self, NNReal.summable_condensed_iff, squarefree_mul, base_pow_length_digits_le, divisors_filter_squarefree, Int.one_shiftLeft, Prime.emultiplicity_pow_self, WittVector.peval_polyOfInterest', choose_le_pow, TruncatedWittVector.commutes', Sylow.pow_dvd_card_of_pow_dvd_card, bitIndices_two_pow_mul, range_pow_padicValNat_subset_divisors', Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent, SimpleGraph.CliqueFree.card_edgeFinset_le, card_pair_lcm_eq, WittVector.nthRemainder_spec, isPRadical_iff, Pell.x_sub_y_dvd_pow, exists_eq_two_pow_mul_odd, Perfection.coeffMonoidHom_pow_p_pow, EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum, prod_pow_factorization_centralBinom, isPrimePow_pow_iff, PadicInt.appr_lt, Submodule.index_smul_le, coprime_pow_left_iff, le_emultiplicity_iff_replicate_subperm_primeFactorsList, dvd_ceilRoot_pow, WeierstrassCurve.coeff_ΨSq, Ideal.absNorm_algebraMap, ordCompl_dvd, sum_properDivisors_prime_nsmul, sq_mul_squarefree_of_pos', primeFactors_prime_pow, IsUpperSet.card_inter_le_finset, ZMod.fieldRange_castHom_eq_bot, digits_base_pow_mul, sq_add_sq_mul, IsPurelyInseparable.exponent_def, emultiplicity_eq_card_pow_dvd, SzemerediRegularity.card_aux₁, Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow, Choose.choose_modEq_prod_range_choose_nat, BitVec.equivFin_apply, Cardinal.preBeth_nat, Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible, finFunctionFinEquiv_apply, finFunctionFinEquiv_single, DirichletCharacter.changeLevel_self, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar, ChevalleyThm.MvPolynomialC.numBound_casesOn_succ, Fintype.card_fun, addOrderOf_eq_prime_pow, PadicInt.cast_toZModPow, neg_one_pow_expChar_pow, WittVector.mul_pow_charP_coeff_succ, ArithmeticFunction.sigma_eq_sum_div, one_half_le_sum_primes_ge_one_div, sub_pow_expChar_pow, WittVector.zmodEquivTrunc_compat, bitIndices_two_pow, Pell.eq_pow_of_pell, pow_two_pow_sub_pow_two_pow, FiniteField.algebraMap_norm_eq_pow_sum, PadicInt.dvd_appr_sub_appr, padicValNat_mul_pow_right, ArithmeticFunction.vonMangoldt_apply_pow, Finset.addEnergy_univ_right, Behrend.exists_large_sphere_aux, wittPolynomial_eq_sum_C_mul_X_pow, padicValNat.maxPowDiv_eq_emultiplicity, Commute.add_pow_prime_pow_eq', WittVector.ghostComponent_teichmuller, bitIndices_twoPowsum, Sylow.card_normalizer_modEq_card, centralBinom_le_of_no_bertrand_prime, ZMod.exists_one_add_mul_pow_prime_pow_eq, isPrimePow_iff_minFac_pow_factorization_eq, ArithmeticFunction.cardFactors_apply_prime_pow, Finset.geomSum_injective, range_pow_padicValNat_subset_divisors, Finset.le_addEnergy_self, ordCompl_self_pow, Finset.sum_condensed_le', digits_append_zeroes_append_digits, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, Pell.xn_ge_a_pow, SimpleGraph.card_topEdgeLabeling, pow_factorization_choose_le, geom_sum_Ico_le, finFunctionFinEquiv_symm_apply_val, tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers, CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux, Prime.sub_one_mul_multiplicity_factorial, prime_pow_pow_totient_ediv_prod, choose_le_two_pow, StrictMono.nat_pow, AlgebraicClosure.hasEnoughRootsOfUnity_pow, equivProdNatSmoothNumbers_apply, Prime.sum_four_squares, ONote.fastGrowing_two, self_div_pow_eq_ofDigits_drop, cyclotomicCharacter.toFun_spec, mapsTo_ofDigits, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, prod_primeFactors_pow_totient_ediv_dvd, PerfectRing.lift_aux, TruncatedWittVector.commutes_symm, dvd_prime_pow, ModEq.pow, coprime_iff_isRelPrime, Int.multiplicity_natAbs, Iic_factorization_prod_pow_injective, padicValNat_eq_emultiplicity, Prime.coprime_pow_of_not_dvd, fermatNumber_succ, Behrend.sum_eq, IsPurelyInseparable.algebraMap_iterateFrobeniusₛₗ, WittVector.nth_mul_coeff', Polynomial.map_iterateFrobenius_expand, Polynomial.roots_X_pow_char_pow_sub_C, minFac_sq_le_self, ArithmeticFunction.carmichael_two_pow_of_ne_two, mem_rootsOfUnity_prime_pow_mul_iff, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', FiniteField.Extension.frob_iterate_apply, IsPurelyInseparable.elemExponent_def, Prime.pow_eq_iff, IsCyclotomicExtension.discr_prime_pow, WittVector.peval_polyOfInterest, IsSelfAdjoint.nnnorm_pow_two_pow, ordCompl_of_not_prime, ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two, IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem, SimpleGraph.mul_card_edgeFinset_turanGraph_le, Behrend.exists_large_sphere, squarefree_iff_factorization_le_one, Finset.card_powerset, card_linearIndependent, Polynomial.expand_pow, List.sum_fixedLengthDigits_sum, IsCyclotomicExtension.discr_prime_pow_ne_two', IsPRadical.pow_mem', multiplicity_eq_zero_of_coprime, IsPrimitiveRoot.toInteger_sub_one_not_dvd_two, LucasLehmer.order_ineq, two_pow_le_of_mem_bitIndices, card_finMulAntidiag_of_squarefree, WeierstrassCurve.natDegree_preΨ, finiteMultiplicity_iff, CommMonoid.coe_primaryComponent, squarefree_mul_iff, ArithmeticFunction.abs_moebius, divisors_eq_image_Iic_factorization_prod_pow, Prime.dvd_choose_pow_iff, Polynomial.IsSeparableContraction.dvd_degree'
instMulOneClass 📖	CompOp	7 math math: divisorsHom_apply, EulerProduct.prod_filter_prime_geometric_eq_tsum_factoredNumbers, EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric, EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers, EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric, Summable.norm_lt_one, PNat.coe_coeMonoidHom
instOne 📖	CompOp	937 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, CategoryTheory.InjectiveResolution.injective, CategoryTheory.InjectiveResolution.Hom.hom'_f, Num.minFac_to_nat, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, CochainComplex.augment_d_succ_succ, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', AlgebraicTopology.DoldKan.P_f_0_eq, FirstOrder.Language.presburger.mul_not_definable, ChainComplex.truncate_map_f, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, groupCohomology.toCocycles_comp_isoCocycles₁_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, ComplexShape.instHasNoLoopNatDown, SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, AlgebraicTopology.NormalizedMooreComplex.obj_d, CochainComplex.quasiIsoAt_πTruncGE, groupCohomology.inhomogeneousCochains.d_def, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, prod_mem_smoothNumbers, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, groupCohomology.cocyclesIso₀_hom_comp_f, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.ProjectiveResolution.quasiIso, CochainComplex.augmentTruncate_inv_f_zero, groupCohomology.eq_d₀₁_comp_inv, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d, ModEq.listProd_one, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, ChainComplex.mkHom_f_0, Holor.cprankMax_upper_bound, Cubic.degree_of_b_eq_zero, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, CochainComplex.quasiIso_truncLEMap_iff, groupCohomology.eq_d₁₂_comp_inv, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', ComplexShape.eulerCharSignsDownNat_χ, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, AlgebraicTopology.DoldKan.identity_N₂, groupHomology.eq_d₃₂_comp_inv, Homotopy.mkInductiveAux₃, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, IsCyclotomicExtension.discr_odd_prime, ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE, CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, groupHomology.chainsMap_id, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id, Rep.barComplex.d_def, CategoryTheory.InjectiveResolution.self_ι, CategoryTheory.InjectiveResolution.iso_hom_naturality, ModEq.listProd_map, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp, PosNum.pred_to_nat, cyclotomicCharacter.toZModPow, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, ChainComplex.mk'_X_0, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, CochainComplex.mk'_X_0, FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Abelian.LeftResolution.chainComplexMap_id, ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE, AlgebraicTopology.DoldKan.PInfty_idem, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, prod_mem_factoredNumbers, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, Num.gcd_to_nat_aux, groupHomology.comp_d₂₁_eq, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, Num.of_to_nat', Num.div_to_nat, Num.sub_to_nat, Num.succ'_to_nat, CochainComplex.ConnectData.d_ofNat, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, CochainComplex.augment_X_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, Num.toNat_injective, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, WithBot.add_eq_two_iff, IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two, AlgebraicTopology.DoldKan.QInfty_idem, ChainComplex.isoHomologyι₀_inv_naturality_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, Num.castNum_eq_bitwise, CochainComplex.truncate_obj_X, PrimeMultiset.prod_ofNatList, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', CochainComplex.ConnectData.map_comp_map, groupCohomology.cochainsMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, ChainComplex.mk_X_2, groupCohomology.comp_d₁₂_eq, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.InjectiveResolution.of_def, CategoryTheory.Preadditive.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.self_π, CategoryTheory.ProjectiveResolution.cochainComplex_d, CochainComplex.instQuasiIsoAtIntπTruncGE, groupHomology.isoCycles₁_inv_comp_iCycles_apply, Polynomial.Splits.degree_le_one_of_irreducible, groupCohomology.dArrowIso₀₁_inv_right, CochainComplex.ConnectData.d_zero_one, groupCohomology.eq_d₂₃_comp_inv_assoc, FormalMultilinearSeries.id_apply_one', groupCohomology.eq_d₂₃_comp_inv_apply, CategoryTheory.InjectiveResolution.complex_d_comp, groupCohomology.eq_d₁₂_comp_inv_apply, ComplexShape.Embedding.embeddingUpInt_areComplementary, Rep.standardComplex.d_eq, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, ZNum.gcd_to_nat, Homotopy.prevD_succ_cochainComplex, CategoryTheory.ProjectiveResolution.sub_extMk, modEq_list_map_prod_iff, CategoryTheory.Functor.mapProjectiveResolution_π, CategoryTheory.instIsIsoToRightDerivedZero', groupHomology.chainsMap_id_f_map_mono, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, CochainComplex.fromSingle₀Equiv_apply_coe, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, PosNum.of_to_nat, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, IsCyclotomicExtension.Rat.discr_prime_pow', IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, Finset.equitableOn_iff_le_le_add_one, CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, Polynomial.degree_X_sub_C, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, groupHomology.chainsMap_f_3_comp_chainsIso₃, ModEq.listProd_map_one, ChainComplex.single₀ObjXSelf, groupHomology.eq_d₂₁_comp_inv, Num.castNum_shiftRight, AlgebraicTopology.DoldKan.QInfty_idem_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc, ComplexShape.ε_down_ℕ, PosNum.size_to_nat, groupCohomology.dArrowIso₀₁_hom_right, AlgebraicTopology.AlternatingFaceMapComplex.map_f, groupCohomology.toCocycles_comp_isoCocycles₂_hom, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two, AlgebraicTopology.DoldKan.QInfty_f, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, Num.size_to_nat, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, ChainComplex.toSingle₀Equiv_apply_coe, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, CategoryTheory.Functor.mapProjectiveResolution_complex, CochainComplex.instQuasiIsoAtIntιTruncLE, AlgebraicTopology.alternatingFaceMapComplex_map_f, SimplicialObject.Splitting.nondegComplex_d, AlgebraicTopology.DoldKan.P_f_idem_assoc, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, Rep.standardComplex.εToSingle₀_comp_eq, ChainComplex.mkHom_f_1, AlgebraicTopology.DoldKan.Γ₀'_obj, groupHomology.inhomogeneousChains.d_def, Num.castNum_xor, ChainComplex.exactAt_succ_single_obj, PosNum.size_eq_natSize, ChainComplex.mk_d_1_0, CochainComplex.quasiIsoAt_ιTruncLE, CategoryTheory.Idempotents.DoldKan.hε, groupCohomology.comp_d₂₃_eq, ChainComplex.truncateAugment_inv_f, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, CategoryTheory.InjectiveResolution.extMk_surjective, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, AlgebraicTopology.DoldKan.QInfty_f_0, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CochainComplex.ConnectData.d_negSucc, CategoryTheory.InjectiveResolution.ι_f_succ, ChainComplex.next_nat_succ, MvPowerSeries.expand_one_apply, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, Set.equitableOn_iff_exists_le_le_add_one, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, PowerSeries.expand_one_apply, CategoryTheory.ProjectiveResolution.extMk_comp_mk₀, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, Homotopy.dNext_zero_chainComplex, Polynomial.Splits.degree_eq_one_of_irreducible, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, groupHomology.chainsMap_f_single, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc, ComplexShape.embeddingUpNat_f, Homotopy.prevD_chainComplex, groupCohomology.cochainsMap_f_map_epi, groupCohomology.comp_d₀₁_eq, AlgebraicTopology.DoldKan.map_Hσ, Num.to_of_nat, CategoryTheory.InjectiveResolution.add_extMk, Num.castNum_shiftLeft, ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, groupHomology.toCycles_comp_isoCycles₁_hom_apply, PosNum.cmp_to_nat_lemma, CochainComplex.mk_d_2_0, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, prevD_nat, CategoryTheory.InjectiveResolution.extMk_zero, AlgebraicTopology.DoldKan.Γ₀_obj_map, CochainComplex.isoHomologyπ₀_inv_naturality, Num.of_to_nat, groupCohomology.cochainsMap_zero, List.nat_divisors_prod, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, PosNum.to_nat_pos, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, groupCohomology.dArrowIso₀₁_inv_left, CochainComplex.exactAt_succ_single_obj, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, groupHomology.map_chainsFunctor_shortExact, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, CochainComplex.augment_X_succ, CochainComplex.mk'_X_1, ZMod.card_units, CategoryTheory.ProjectiveResolution.extMk_hom, groupHomology.eq_d₃₂_comp_inv_apply, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, CochainComplex.single₀_map_f_zero, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, PosNum.pred'_to_nat, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, PosNum.of_to_nat', ChainComplex.augmentTruncate_inv_f_succ, Polynomial.degree_X_le, groupCohomology.cochainsMap_id_comp, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, ChainComplex.augment_X_succ, CochainComplex.ConnectData.map_f, ChainComplex.quasiIsoAt₀_iff, groupCohomology.cochainsMap_comp_assoc, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, WithBot.add_eq_one_iff, groupHomology.chainsMap_f_map_epi, CochainComplex.ConnectData.d_sub_two_sub_one, PosNum.bit_to_nat, groupHomology.isoShortComplexH1_hom, IsPrimitiveRoot.finite_quotient_span_sub_one', CochainComplex.augment_d_zero_one, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, groupCohomology.isoCocycles₂_hom_comp_i, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, IsPrimitiveRoot.finite_quotient_span_sub_one, MvPowerSeries.expand_one, CategoryTheory.ProjectiveResolution.of_def, Num.castNum_or, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.ProjectiveResolution.iso_hom_naturality, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CategoryTheory.ProjectiveResolution.π_f_succ, groupCohomology.dArrowIso₀₁_hom_left, AlgebraicTopology.inclusionOfMooreComplex_app, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, Polynomial.Splits.def, PosNum.to_nat_inj, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, AlgebraicTopology.DoldKan.P_f_idem, WithBot.add_eq_three_iff, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, groupCohomology.eq_d₀₁_comp_inv_apply, AlgebraicTopology.DoldKan.PInfty_idem_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, Lagrange.degree_basisDivisor_of_ne, CochainComplex.ConnectData.restrictionLEIso_inv_f, CategoryTheory.ProjectiveResolution.add_extMk, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupHomology.chainsFunctor_obj, Polynomial.splits_iff, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, CategoryTheory.ProjectiveResolution.Hom.hom'_f, CochainComplex.quasiIso_truncGEMap_iff, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, ChainComplex.isIso_descOpcycles_iff, Num.cast_to_nat, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, SimplicialObject.Splitting.nondegComplex_X, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', ComplexShape.instIsRelIffNatIntEmbeddingDownNat, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy, groupHomology.d₁₀ArrowIso_inv_right, ArithmeticFunction.natCoe_one, chineseRemainderOfList_modEq_unique, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0, Num.castNum_ldiff, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', MvPolynomial.weightedTotalDegree_one, CategoryTheory.InjectiveResolution.extMk_eq_zero_iff, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, ChainComplex.mk_X_0, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, groupHomology.chainsMap_id_f_map_epi, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, CochainComplex.truncateAugment_inv_f, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, IsCyclotomicExtension.discr_prime_pow_ne_two, AlgebraicTopology.DoldKan.map_PInfty_f, AlgebraicTopology.DoldKan.P_succ, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, CochainComplex.ConnectData.X_zero, groupCohomology.cochainsMap_id_f_map_mono, groupHomology.chainsMap_id_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, Num.succ_to_nat, Polynomial.degree_C_lt, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, SimplicialObject.Split.nondegComplexFunctor_map_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, groupHomology.isoCycles₂_hom_comp_i_apply, AlgebraicTopology.DoldKan.Hσ_eq_zero, CochainComplex.ConnectData.d₀_comp, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, PosNum.to_int_eq_succ_pred, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, AlgebraicTopology.normalizedMooreComplex_objD, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, PosNum.natSize_to_nat, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, CategoryTheory.InjectiveResolution.self_cocomplex, PosNum.div'_to_nat, CategoryTheory.ProjectiveResolution.lift_commutes_zero, groupCohomology.isoCocycles₁_inv_comp_iCocycles, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, groupHomology.eq_d₂₁_comp_inv_assoc, ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', groupHomology.cyclesIso₀_inv_comp_iCycles, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, Num.castNum_and, CochainComplex.mkHom_f_succ_succ, AlgebraicTopology.DoldKan.Q_idem_assoc, AlgebraicTopology.DoldKan.PInfty_f, ChainComplex.isoHomologyι₀_inv_naturality, AlgebraicTopology.DoldKan.Γ₀_map_app, PosNum.lt_to_nat, Polynomial.degree_X_sub_C_le, Num.ofZNum_toNat, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, AlgebraicTopology.DoldKan.Q_f_0_eq, Polynomial.degree_C_mul_X_le, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, CochainComplex.ConnectData.X_ofNat, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, AlgebraicTopology.DoldKan.QInfty_f_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, CochainComplex.instQuasiIsoIntιTruncLEOfIsLE, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', withBotSucc_one, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, ChainComplex.next_nat_zero, ComplexShape.boundaryGE_embeddingUpIntGE_iff, CochainComplex.truncate_map_f, ChainComplex.augmentTruncate_hom_f_succ, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, CochainComplex.prev_nat_succ, IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two, WithBot.one_le_iff_zero_lt, CategoryTheory.ProjectiveResolution.exact_succ, CategoryTheory.ProjectiveResolution.π'_f_zero, CochainComplex.isIso_liftCycles_iff, AlgebraicTopology.DoldKan.P_f_naturality_assoc, PosNum.le_to_nat, CategoryTheory.InjectiveResolution.desc_commutes, CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp, PosNum.cast_to_nat, AlgebraicTopology.DoldKan.map_P, Homotopy.mkCoinductiveAux₂_add_one, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, groupHomology.chainsMap_f_map_mono, CategoryTheory.InjectiveResolution.desc_commutes_assoc, groupHomology.eq_d₁₀_comp_inv, Num.lt_to_nat, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, groupHomology.isoShortComplexH1_inv, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, groupHomology.eq_d₁₀_comp_inv_assoc, Num.ppred_to_nat, xInTermsOfW_vars_subset, CochainComplex.ConnectData.restrictionLEIso_hom_f, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, MvPolynomial.weightedHomogeneousSubmodule_one, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, AlgebraicTopology.DoldKan.P_idem, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, groupCohomology.cochainsMap_f, CategoryTheory.ProjectiveResolution.complex_d_succ_comp, AlgebraicTopology.DoldKan.Γ₀.map_app, Homotopy.dNext_succ_chainComplex, Homotopy.mkCoinductiveAux₂_zero, groupHomology.chainsMap_comp, Polynomial.Splits.splits, AlgebraicTopology.DoldKan.natTransP_app, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, Num.bit_to_nat, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, PosNum.mod'_to_nat, SimplicialObject.Split.nondegComplexFunctor_obj, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, AlgebraicTopology.DoldKan.N₁_obj_X, AlgebraicTopology.map_alternatingFaceMapComplex, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc, groupCohomology.cocyclesMk₁_eq, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.quasiIso_πTruncGE_iff, CategoryTheory.ProjectiveResolution.hasHomology, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, PosNum.mul_to_nat, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_obj, AlgebraicTopology.DoldKan.Q_is_eventually_constant, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, CategoryTheory.ProjectiveResolution.extMk_zero, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, groupHomology.toCycles_comp_isoCycles₂_hom_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, Finset.equitableOn_iff, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, Cubic.degree_of_c_ne_zero, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, ChainComplex.mk'_d, CategoryTheory.ProjectiveResolution.self_complex, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.InjectiveResolution.sub_extMk, groupHomology.eq_d₃₂_comp_inv_assoc, ChainComplex.truncateAugment_hom_f, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, PosNum.add_to_nat, AlgebraicTopology.DoldKan.Q_succ, AlgebraicTopology.DoldKan.natTransPInfty_f_app, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, Rep.standardComplex.d_comp_ε, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, modEq_list_prod_iff, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ, Polynomial.degree_X, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.Functor.leftDerived_map_eq, MeasureTheory.upcrossingsBefore_eq_sum, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, ZNum.abs_to_nat, CochainComplex.ConnectData.X_negOne, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, CategoryTheory.Abelian.DoldKan.equivalence_inverse, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, groupHomology.isoShortComplexH2_hom, ChainComplex.augmentTruncate_hom_f_zero, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, PosNum.minFacAux_to_nat, cast_list_prod, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, CochainComplex.ConnectData.X_negSucc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, ComplexShape.instIsRelIffNatIntEmbeddingUpNat, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff, AlgebraicTopology.DoldKan.hσ'_eq, ChainComplex.toSingle₀Equiv_symm_apply_f_zero, groupHomology.chainsMap_f_2_comp_chainsIso₂, AlgebraicTopology.DoldKan.MorphComponents.id_a, groupHomology.pOpcycles_comp_opcyclesIso_hom, Num.dvd_to_nat, WithBot.lt_one_iff_le_zero, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, ChainComplex.instHasHomologyNatObjAlternatingConst, CategoryTheory.InjectiveResolution.mk₀_comp_extMk, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, AlgebraicTopology.DoldKan.PInfty_f_0, groupCohomology.eq_d₂₃_comp_inv, groupCohomology.cochainsMap_f_map_mono, minpoly.degree_eq_one_iff, Homotopy.mkCoinductiveAux₃, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, CategoryTheory.InjectiveResolution.extMk_hom, groupCohomology.isoShortComplexH1_hom, TruncatedWittVector.card_zmod, CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor, AlgebraicTopology.DoldKan.PInfty_f_naturality, CategoryTheory.InjectiveResolution.cochainComplex_d_assoc, AlgebraicTopology.DoldKan.hσ'_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles, ComplexShape.eulerCharSignsUpNat_χ, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, CochainComplex.quasiIso_ιTruncLE_iff, ChainComplex.isIso_homologyι₀, ChainComplex.truncate_obj_d, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, inhomogeneousCochains.d_eq, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, IsSepClosed.degree_eq_one_of_irreducible, CochainComplex.quasiIsoAt₀_iff, Rep.FiniteCyclicGroup.resolution_complex, PosNum.cmp_to_nat, groupHomology.chainsFunctor_map, cyclotomicCharacter.toFun_apply, groupCohomology.cocyclesMk₂_eq, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, quadraticChar_odd_prime, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, ComplexShape.embeddingUpIntLE_f, groupCohomology.cochainsMap_id_f_map_epi, groupHomology.chainsMap_f_hom, CochainComplex.ConnectData.restrictionGEIso_inv_f, AlgebraicTopology.DoldKan.P_is_eventually_constant, AlgebraicTopology.DoldKan.map_Q, CategoryTheory.ProjectiveResolution.extMk_surjective, cyclotomicCharacter.toZModPow_toFun, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, CochainComplex.ConnectData.map_id, AlgebraicTopology.DoldKan.PInfty_f_idem, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, AlgebraicTopology.DoldKan.N₂_obj_p_f, Polynomial.degree_eq_one_of_irreducible_of_splits, groupHomology.cyclesMk₁_eq, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc, AlgebraicTopology.DoldKan.σ_comp_PInfty, CochainComplex.mkHom_f_1, ComplexShape.embeddingDownNat_f, groupCohomology.isoCocycles₁_hom_comp_i, CochainComplex.augmentTruncate_inv_f_succ, legendreSym.card_sqrts, AlgebraicTopology.NormalizedMooreComplex.obj_X, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, AlgebraicTopology.DoldKan.N₂_obj_X_X, CategoryTheory.Functor.rightDerived_map_eq, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, Rep.standardComplex.instQuasiIsoNatεToSingle₀, CochainComplex.mk_X_2, Rep.standardComplex.x_projective, Homotopy.prevD_zero_cochainComplex, CochainComplex.mkHom_f_0, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, CochainComplex.ConnectData.d₀_comp_assoc, ChainComplex.fromSingle₀Equiv_apply, TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor, CategoryTheory.InjectiveResolution.desc_commutes_zero, Rep.FiniteCyclicGroup.resolution_quasiIso, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, AlgebraicTopology.DoldKan.P_zero, CochainComplex.augmentTruncate_hom_f_succ, groupCohomology.cochainsMap_f_hom, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, Rep.standardComplex.d_apply, PosNum.divMod_to_nat_aux, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, ChainComplex.chainComplex_d_succ_succ_zero, CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, CochainComplex.ConnectData.homologyMap_map_of_eq_succ, AlgebraicTopology.alternatingCofaceMapComplex_map, WithBot.add_one_le_of_lt, CategoryTheory.Idempotents.DoldKan.equivalence_functor, Option.card_toFinset, AlgebraicTopology.DoldKan.N₂_obj_X_d, Polynomial.degree_eq_one_of_irreducible_of_root, Polynomial.degree_mul_X, PosNum.divMod_to_nat, groupHomology.isoCycles₁_hom_comp_i_assoc, CategoryTheory.Abelian.DoldKan.equivalence_functor, xInTermsOfW_vars_aux, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, ChainComplex.augment_d_succ_succ, groupCohomology.isoShortComplexH2_hom, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CategoryTheory.ProjectiveResolution.exact₀, CategoryTheory.InjectiveResolution.hasHomology, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CochainComplex.fromSingle₀Equiv_symm_apply_f_zero, CochainComplex.ConnectData.comp_d₀, ChainComplex.augmentTruncate_inv_f_zero, Num.cmp_to_nat, CochainComplex.truncateAugment_hom_f, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, FirstOrder.Language.presburger.definable₁_iff_ultimately_periodic, ComplexShape.instIsTruncLENatIntEmbeddingDownNat, Num.to_nat_to_int, CategoryTheory.InjectiveResolution.neg_extMk, CategoryTheory.Idempotents.DoldKan.Γ_map_app, CategoryTheory.ProjectiveResolution.projective, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, Num.ofZNum'_toNat, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, ChainComplex.alternatingConst_exactAt, CochainComplex.toSingle₀Equiv_apply, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, groupHomology.isoCycles₁_inv_comp_iCycles, chineseRemainderOfList_lt_prod, groupHomology.chainsMap_zero, groupHomology.isoShortComplexH2_inv, PowerSeries.expand_one, CochainComplex.cochainComplex_d_succ_succ_zero, groupHomology.toCycles_comp_isoCycles₁_hom, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, Cubic.degree_of_b_eq_zero', AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, Num.natSize_to_nat, Num.le_to_nat, Cubic.degree_of_c_ne_zero', groupCohomology.iCocycles_mk, AlgebraicTopology.DoldKan.QInfty_f_idem, groupHomology.isoCycles₂_hom_comp_i, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, groupHomology.isoCycles₂_inv_comp_iCycles, groupCohomology.map_cochainsFunctor_shortExact, ChainComplex.mk'_X_1, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, CategoryTheory.InjectiveResolution.exact_succ, ChainComplex.mk_d, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, Polynomial.degree_linear_le, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, CochainComplex.ConnectData.comp_d₀_assoc, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, CategoryTheory.InjectiveResolution.instMonoFNatι, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero, PosNum.dvd_to_nat, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, groupHomology.d₁₀ArrowIso_hom_right, Homotopy.dNext_cochainComplex, CochainComplex.mk'_d_1_0, jacobiSym.list_prod_right, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, IsPrimitiveRoot.zeta_sub_one_prime, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, ComplexShape.instHasNoLoopNatUp, PosNum.to_nat_to_int, Num.mod_to_nat, groupCohomology.isoCocycles₂_hom_comp_i_apply, Num.to_nat_inj, ChainComplex.mk'_d_1_0, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, Polynomial.degree_C_mul_X, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CategoryTheory.ProjectiveResolution.iso_inv_naturality, Num.gcd_to_nat, groupHomology.inhomogeneousChains.d_eq, groupHomology.eq_d₂₁_comp_inv_apply, Num.castNum_testBit, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ, groupCohomology.cochainsFunctor_map, groupHomology.iCycles_mk, AlgebraicTopology.DoldKan.decomposition_Q, Num.size_eq_natSize, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, IsCyclotomicExtension.Rat.discr_odd_prime', groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, ComplexShape.embeddingUpIntGE_f, Num.mul_to_nat, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, AlgebraicTopology.DoldKan.Q_f_idem_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, AlgebraicTopology.DoldKan.Γ₂N₁_inv, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc, Polynomial.splits_iff_splits, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, groupCohomology.cocyclesMk₀_eq, AlgebraicTopology.DoldKan.Q_f_naturality, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, AlgebraicTopology.DoldKan.Q_zero, groupHomology.lsingle_comp_chainsMap_f_assoc, ChainComplex.mkHom_f_succ_succ, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, IsAlgClosed.degree_eq_one_of_irreducible, ChainComplex.truncate_obj_X, groupCohomology.isoShortComplexH1_inv, AlgebraicTopology.DoldKan.identity_N₂_objectwise, CochainComplex.single₀_obj_zero, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, AlgebraicTopology.inclusionOfMooreComplexMap_f, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, CategoryTheory.Idempotents.DoldKan.hη, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, coprime_list_prod_right_iff, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', Module.rankAtStalk_self, dNext_nat, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, groupCohomology.cochainsMap_id_comp_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality, Holor.cprank_upper_bound, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, CategoryTheory.ProjectiveResolution.neg_extMk, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, PosNum.to_nat_eq_succ_pred, AlgebraicTopology.DoldKan.map_hσ', CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, AlgebraicTopology.DoldKan.N₂_map_f_f, CochainComplex.truncate_obj_d, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, IsLinearSet.definable, groupCohomology.eq_d₁₂_comp_inv_assoc, AlgebraicTopology.DoldKan.P_f_naturality, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, CategoryTheory.SimplicialObject.Homotopy.map_homology_eq, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', AlgebraicTopology.DoldKan.N₁Γ₀_app, CochainComplex.isIso_homologyπ₀, groupCohomology.isoShortComplexH2_inv, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, groupCohomology.isoCocycles₂_hom_comp_i_assoc, CochainComplex.augmentTruncate_hom_f_zero, groupHomology.eq_d₁₀_comp_inv_apply, Homotopy.mkInductiveAux₂_zero, ChainComplex.alternatingConst_map_f, CategoryTheory.Idempotents.DoldKan.N_map, ChainComplex.single₀_obj_zero, Num.pred_to_nat, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, CategoryTheory.InjectiveResolution.quasiIso, CategoryTheory.InjectiveResolution.iso_inv_naturality, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, CochainComplex.mk_d_1_0, Set.equitableOn_iff_exists_eq_eq_add_one, FirstOrder.Language.presburger.term_realize_eq_add_dotProduct, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, AlgebraicTopology.DoldKan.hσ'_eq', groupCohomology.eq_d₀₁_comp_inv_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, Polynomial.degree_linear, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom, prod_primeFactorsList, groupCohomology.isoCocycles₁_hom_comp_i_assoc, CategoryTheory.InjectiveResolution.descFOne_zero_comm, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinear, ChainComplex.single₀_map_f_zero, ChainComplex.alternatingConst_obj, IsSemilinearSet.definable, ChainComplex.mk_d_2_1, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, AlgebraicTopology.DoldKan.Γ₀'_map_f, ComplexShape.boundaryLE_embeddingUpIntLE_iff, PosNum.succ_to_nat, Rep.FiniteCyclicGroup.resolution.π_f, groupCohomology.cochainsFunctor_obj, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CochainComplex.instQuasiIsoIntπTruncGEOfIsGE, FirstOrder.Language.presburger.definable_iff_isSemilinearSet, List.prod_nat_mod, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀, coprime_list_prod_left_iff, CochainComplex.single₀ObjXSelf, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, CochainComplex.prev_nat_zero, AlgebraicTopology.DoldKan.Γ₂N₂_inv, groupHomology.isoCycles₂_hom_comp_i_assoc, CochainComplex.mk_X_0, groupHomology.comp_d₃₂_eq, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, groupHomology.chainsMap_f_0_comp_chainsIso₀, AlgebraicTopology.normalizedMooreComplex_obj, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', AlgebraicTopology.DoldKan.natTransQ_app, ChainComplex.augment_X_zero, IsCyclotomicExtension.discr_prime_pow, CategoryTheory.ProjectiveResolution.complex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp_assoc, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, IsPrimitiveRoot.zeta_sub_one_prime', Set.equitableOn_iff_exists_image_subset_icc, ComplexShape.instIsTruncGENatIntEmbeddingUpNat, CategoryTheory.instIsIsoFromLeftDerivedZero', PosNum.minFac_to_nat, IsCyclotomicExtension.discr_prime_pow_ne_two', Polynomial.degree_X_add_C, Num.add_to_nat, ChainComplex.mk_X_1, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, CochainComplex.mk_X_1, IsPrimitiveRoot.toInteger_sub_one_not_dvd_two, groupHomology.chainsMap_f, ChainComplex.augment_d_one_zero, AlgebraicTopology.DoldKan.PInfty_add_QInfty, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, AlgebraicTopology.DoldKan.Q_f_idem, groupCohomology.cochainsMap_id, CategoryTheory.InjectiveResolution.cochainComplex_d, CochainComplex.ConnectData.restrictionGEIso_hom_f, Homotopy.mkInductiveAux₂_add_one
instSemigroup 📖	CompOp	3 math math: DirichletCharacter.changeLevel_trans, ZMod.unitsMap_comp, ZMod.castHom_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddTorsionFree 📖	mathematical	—	IsAddTorsionFree AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid	—	—
instIsMulTorsionFree 📖	mathematical	—	IsMulTorsionFree CommMonoid.toMonoid instCommMonoid	—	—
nsmul_eq_mul 📖	mathematical	—	AddMonoid.toNSMul instAddMonoid	—	—

---

← Back to Index